Metamath Proof Explorer


Theorem intprOLD

Description: Obsolete version of intpr as of 1-Sep-2024. (Contributed by NM, 14-Oct-1999) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses intpr.1 𝐴 ∈ V
intpr.2 𝐵 ∈ V
Assertion intprOLD { 𝐴 , 𝐵 } = ( 𝐴𝐵 )

Proof

Step Hyp Ref Expression
1 intpr.1 𝐴 ∈ V
2 intpr.2 𝐵 ∈ V
3 19.26 ( ∀ 𝑦 ( ( 𝑦 = 𝐴𝑥𝑦 ) ∧ ( 𝑦 = 𝐵𝑥𝑦 ) ) ↔ ( ∀ 𝑦 ( 𝑦 = 𝐴𝑥𝑦 ) ∧ ∀ 𝑦 ( 𝑦 = 𝐵𝑥𝑦 ) ) )
4 vex 𝑦 ∈ V
5 4 elpr ( 𝑦 ∈ { 𝐴 , 𝐵 } ↔ ( 𝑦 = 𝐴𝑦 = 𝐵 ) )
6 5 imbi1i ( ( 𝑦 ∈ { 𝐴 , 𝐵 } → 𝑥𝑦 ) ↔ ( ( 𝑦 = 𝐴𝑦 = 𝐵 ) → 𝑥𝑦 ) )
7 jaob ( ( ( 𝑦 = 𝐴𝑦 = 𝐵 ) → 𝑥𝑦 ) ↔ ( ( 𝑦 = 𝐴𝑥𝑦 ) ∧ ( 𝑦 = 𝐵𝑥𝑦 ) ) )
8 6 7 bitri ( ( 𝑦 ∈ { 𝐴 , 𝐵 } → 𝑥𝑦 ) ↔ ( ( 𝑦 = 𝐴𝑥𝑦 ) ∧ ( 𝑦 = 𝐵𝑥𝑦 ) ) )
9 8 albii ( ∀ 𝑦 ( 𝑦 ∈ { 𝐴 , 𝐵 } → 𝑥𝑦 ) ↔ ∀ 𝑦 ( ( 𝑦 = 𝐴𝑥𝑦 ) ∧ ( 𝑦 = 𝐵𝑥𝑦 ) ) )
10 1 clel4 ( 𝑥𝐴 ↔ ∀ 𝑦 ( 𝑦 = 𝐴𝑥𝑦 ) )
11 2 clel4 ( 𝑥𝐵 ↔ ∀ 𝑦 ( 𝑦 = 𝐵𝑥𝑦 ) )
12 10 11 anbi12i ( ( 𝑥𝐴𝑥𝐵 ) ↔ ( ∀ 𝑦 ( 𝑦 = 𝐴𝑥𝑦 ) ∧ ∀ 𝑦 ( 𝑦 = 𝐵𝑥𝑦 ) ) )
13 3 9 12 3bitr4i ( ∀ 𝑦 ( 𝑦 ∈ { 𝐴 , 𝐵 } → 𝑥𝑦 ) ↔ ( 𝑥𝐴𝑥𝐵 ) )
14 vex 𝑥 ∈ V
15 14 elint ( 𝑥 { 𝐴 , 𝐵 } ↔ ∀ 𝑦 ( 𝑦 ∈ { 𝐴 , 𝐵 } → 𝑥𝑦 ) )
16 elin ( 𝑥 ∈ ( 𝐴𝐵 ) ↔ ( 𝑥𝐴𝑥𝐵 ) )
17 13 15 16 3bitr4i ( 𝑥 { 𝐴 , 𝐵 } ↔ 𝑥 ∈ ( 𝐴𝐵 ) )
18 17 eqriv { 𝐴 , 𝐵 } = ( 𝐴𝐵 )