Metamath Proof Explorer

Theorem prexOLD

Description: Obsolete version of prex as of 6-Mar-2026. (Contributed by NM, 15-Jul-1993) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion prexOLD ⊢ A B ∈ V

Proof

Step Hyp Ref Expression
1 preq2 ⊢ y = B → x y = x B
2 1 eleq1d ⊢ y = B → x y ∈ V ↔ x B ∈ V
3 zfpair2 ⊢ x y ∈ V
4 2 3 vtoclg ⊢ B ∈ V → x B ∈ V
5 preq1 ⊢ x = A → x B = A B
6 5 eleq1d ⊢ x = A → x B ∈ V ↔ A B ∈ V
7 4 6 imbitrid ⊢ x = A → B ∈ V → A B ∈ V
8 7 vtocleg ⊢ A ∈ V → B ∈ V → A B ∈ V
9 prprc1 ⊢ ¬ A ∈ V → A B = B
10 snexOLD ⊢ B ∈ V
11 9 10 eqeltrdi ⊢ ¬ A ∈ V → A B ∈ V
12 prprc2 ⊢ ¬ B ∈ V → A B = A
13 snexOLD ⊢ A ∈ V
14 12 13 eqeltrdi ⊢ ¬ B ∈ V → A B ∈ V
15 8 11 14 pm2.61nii ⊢ A B ∈ V