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	⊢ { 𝐴 , 𝐵 } ∈ V

Proof

Step	Hyp	Ref	Expression
1		preq2	⊢ ( 𝑦 = 𝐵 → { 𝑥 , 𝑦 } = { 𝑥 , 𝐵 } )
2	1	eleq1d	⊢ ( 𝑦 = 𝐵 → ( { 𝑥 , 𝑦 } ∈ V ↔ { 𝑥 , 𝐵 } ∈ V ) )
3		zfpair2	⊢ { 𝑥 , 𝑦 } ∈ V
4	2 3	vtoclg	⊢ ( 𝐵 ∈ V → { 𝑥 , 𝐵 } ∈ V )
5		preq1	⊢ ( 𝑥 = 𝐴 → { 𝑥 , 𝐵 } = { 𝐴 , 𝐵 } )
6	5	eleq1d	⊢ ( 𝑥 = 𝐴 → ( { 𝑥 , 𝐵 } ∈ V ↔ { 𝐴 , 𝐵 } ∈ V ) )
7	4 6	imbitrid	⊢ ( 𝑥 = 𝐴 → ( 𝐵 ∈ V → { 𝐴 , 𝐵 } ∈ V ) )
8	7	vtocleg	⊢ ( 𝐴 ∈ V → ( 𝐵 ∈ V → { 𝐴 , 𝐵 } ∈ V ) )
9		prprc1	⊢ ( ¬ 𝐴 ∈ V → { 𝐴 , 𝐵 } = { 𝐵 } )
10		snexOLD	⊢ { 𝐵 } ∈ V
11	9 10	eqeltrdi	⊢ ( ¬ 𝐴 ∈ V → { 𝐴 , 𝐵 } ∈ V )
12		prprc2	⊢ ( ¬ 𝐵 ∈ V → { 𝐴 , 𝐵 } = { 𝐴 } )
13		snexOLD	⊢ { 𝐴 } ∈ V
14	12 13	eqeltrdi	⊢ ( ¬ 𝐵 ∈ V → { 𝐴 , 𝐵 } ∈ V )
15	8 11 14	pm2.61nii	⊢ { 𝐴 , 𝐵 } ∈ V