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

Metamath Proof Explorer

Theorem unexbOLD

Description: Obsolete version of unexb as of 21-Jul-2025. (Contributed by NM, 11-Jun-1998) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion unexbOLD ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ↔ ( 𝐴 ∪ 𝐵 ) ∈ V )

Proof

Step Hyp Ref Expression
1 uneq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∪ 𝑦 ) = ( 𝐴 ∪ 𝑦 ) )
2 1 eleq1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ∪ 𝑦 ) ∈ V ↔ ( 𝐴 ∪ 𝑦 ) ∈ V ) )
3 uneq2 ⊢ ( 𝑦 = 𝐵 → ( 𝐴 ∪ 𝑦 ) = ( 𝐴 ∪ 𝐵 ) )
4 3 eleq1d ⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 ∪ 𝑦 ) ∈ V ↔ ( 𝐴 ∪ 𝐵 ) ∈ V ) )
5 vex ⊢ 𝑥 ∈ V
6 vex ⊢ 𝑦 ∈ V
7 5 6 unex ⊢ ( 𝑥 ∪ 𝑦 ) ∈ V
8 2 4 7 vtocl2g ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐴 ∪ 𝐵 ) ∈ V )
9 ssun1 ⊢ 𝐴 ⊆ ( 𝐴 ∪ 𝐵 )
10 ssexg ⊢ ( ( 𝐴 ⊆ ( 𝐴 ∪ 𝐵 ) ∧ ( 𝐴 ∪ 𝐵 ) ∈ V ) → 𝐴 ∈ V )
11 9 10 mpan ⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ V → 𝐴 ∈ V )
12 ssun2 ⊢ 𝐵 ⊆ ( 𝐴 ∪ 𝐵 )
13 ssexg ⊢ ( ( 𝐵 ⊆ ( 𝐴 ∪ 𝐵 ) ∧ ( 𝐴 ∪ 𝐵 ) ∈ V ) → 𝐵 ∈ V )
14 12 13 mpan ⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ V → 𝐵 ∈ V )
15 11 14 jca ⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ V → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
16 8 15 impbii ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ↔ ( 𝐴 ∪ 𝐵 ) ∈ V )