Theorem opeq1 3763

Description: Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)

Assertion

Ref	Expression
opeq1	⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)

Proof of Theorem opeq1

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq1 2233	. . . . . 6 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi1d 462	. . . . 5 ⊢ (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V)))
3		sneq 3592	. . . . . . 7 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
4		preq1 3658	. . . . . . 7 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
5	3, 4	preq12d 3666	. . . . . 6 ⊢ (𝐴 = 𝐵 → {{𝐴}, {𝐴, 𝐶}} = {{𝐵}, {𝐵, 𝐶}})
6	5	eleq2d 2240	. . . . 5 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ {{𝐴}, {𝐴, 𝐶}} ↔ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}}))
7	2, 6	anbi12d 470	. . . 4 ⊢ (𝐴 = 𝐵 → (((𝐴 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}}) ↔ ((𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}})))
8		df-3an 975	. . . 4 ⊢ ((𝐴 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}}) ↔ ((𝐴 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}}))
9		df-3an 975	. . . 4 ⊢ ((𝐵 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}}) ↔ ((𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}}))
10	7, 8, 9	3bitr4g 222	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}}) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}})))
11	10	abbidv 2288	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ (𝐴 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}})} = {𝑥 ∣ (𝐵 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}})})
12		df-op 3590	. 2 ⊢ ⟨𝐴, 𝐶⟩ = {𝑥 ∣ (𝐴 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}})}
13		df-op 3590	. 2 ⊢ ⟨𝐵, 𝐶⟩ = {𝑥 ∣ (𝐵 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}})}
14	11, 12, 13	3eqtr4g 2228	1 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 973   = wceq 1348   ∈ wcel 2141  {cab 2156  Vcvv 2730  {csn 3581  {cpr 3582  ⟨cop 3584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-un 3125  df-sn 3587  df-pr 3588  df-op 3590

This theorem is referenced by:  opeq12  3765  opeq1i  3766  opeq1d  3769  oteq1  3772  breq1  3990  cbvopab1  4060  cbvopab1s  4062  opthg  4221  eqvinop  4226  opelopabsb  4243  opelxp  4639  elvvv  4672  opabid2  4740  opeliunxp2  4749  elsnres  4926  elimasng  4977  rnxpid  5043  dmsnopg  5080  cnvsng  5094  elxp4  5096  elxp5  5097  funopg  5230  f1osng  5481  dmfco  5562  fvelrn  5625  fsng  5667  fvsng  5690  funfvima3  5727  oveq1  5858  oprabid  5883  dfoprab2  5898  cbvoprab1  5923  opabex3d  6098  opabex3  6099  op1stg  6127  op2ndg  6128  oprssdmm  6148  dfoprab4f  6170  cnvoprab  6211  opeliunxp2f  6215  tfr1onlemaccex  6325  tfrcllemaccex  6338  elixpsn  6711  fundmen  6782  xpsnen  6797  xpassen  6806  xpf1o  6820  ltexnqq  7363  archnqq  7372  prarloclemarch2  7374  prarloclemlo  7449  prarloclem3  7452  prarloclem5  7455  caucvgprlemnkj  7621  caucvgprlemnbj  7622  caucvgprlemm  7623  caucvgprlemdisj  7629  caucvgprlemloc  7630  caucvgprlemcl  7631  caucvgprlemladdfu  7632  caucvgprlemladdrl  7633  caucvgprlem1  7634  caucvgprlem2  7635  caucvgpr  7637  caucvgprprlemell  7640  caucvgprprlemelu  7641  caucvgprprlemcbv  7642  caucvgprprlemval  7643  caucvgprprlemnkeqj  7645  caucvgprprlemmu  7650  caucvgprprlemopl  7652  caucvgprprlemlol  7653  caucvgprprlemopu  7654  caucvgprprlemloc  7658  caucvgprprlemclphr  7660  caucvgprprlemexbt  7661  caucvgprprlem1  7664  caucvgprprlem2  7665  caucvgsr  7757  suplocsrlemb  7761  suplocsrlempr  7762  suplocsrlem  7763  suplocsr  7764  elrealeu  7784  pitonn  7803  nntopi  7849  axcaucvglemval  7852  axcaucvg  7855  axpre-suploclemres  7856  fsum2dlemstep  11390  fprod2dlemstep  11578  cnmpt21  13050