This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem disjlem19

Description: Lemma for disjdmqseq , partim2 and petlem via disjdmqs , (general version of the former prtlem19 ). (Contributed by Peter Mazsa, 16-Sep-2021)

Ref Expression
Assertion disjlem19 ⊢ A ∈ V → Disj R → x ∈ dom ⁡ R ∧ A ∈ x R → x R = A ≀ R

Proof

Step Hyp Ref Expression
1 disjlem18 ⊢ A ∈ V ∧ z ∈ V → Disj R → x ∈ dom ⁡ R ∧ A ∈ x R → z ∈ x R ↔ A ≀ R z
2 1 elvd ⊢ A ∈ V → Disj R → x ∈ dom ⁡ R ∧ A ∈ x R → z ∈ x R ↔ A ≀ R z
3 2 imp31 ⊢ A ∈ V ∧ Disj R ∧ x ∈ dom ⁡ R ∧ A ∈ x R → z ∈ x R ↔ A ≀ R z
4 elecALTV ⊢ A ∈ V ∧ z ∈ V → z ∈ A ≀ R ↔ A ≀ R z
5 4 elvd ⊢ A ∈ V → z ∈ A ≀ R ↔ A ≀ R z
6 5 ad2antrr ⊢ A ∈ V ∧ Disj R ∧ x ∈ dom ⁡ R ∧ A ∈ x R → z ∈ A ≀ R ↔ A ≀ R z
7 3 6 bitr4d ⊢ A ∈ V ∧ Disj R ∧ x ∈ dom ⁡ R ∧ A ∈ x R → z ∈ x R ↔ z ∈ A ≀ R
8 7 eqrdv ⊢ A ∈ V ∧ Disj R ∧ x ∈ dom ⁡ R ∧ A ∈ x R → x R = A ≀ R
9 8 exp31 ⊢ A ∈ V → Disj R → x ∈ dom ⁡ R ∧ A ∈ x R → x R = A ≀ R