Theorem opeq1 3885

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 2297	. . . . . 6 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi1d 465	. . . . 5 ⊢ (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V)))
3		sneq 3702	. . . . . . 7 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
4		preq1 3770	. . . . . . 7 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
5	3, 4	preq12d 3778	. . . . . 6 ⊢ (𝐴 = 𝐵 → {{𝐴}, {𝐴, 𝐶}} = {{𝐵}, {𝐵, 𝐶}})
6	5	eleq2d 2304	. . . . 5 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ {{𝐴}, {𝐴, 𝐶}} ↔ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}}))
7	2, 6	anbi12d 473	. . . 4 ⊢ (𝐴 = 𝐵 → (((𝐴 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}}) ↔ ((𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}})))
8		df-3an 1007	. . . 4 ⊢ ((𝐴 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}}) ↔ ((𝐴 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}}))
9		df-3an 1007	. . . 4 ⊢ ((𝐵 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}}) ↔ ((𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}}))
10	7, 8, 9	3bitr4g 223	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}}) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}})))
11	10	abbidv 2354	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ (𝐴 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}})} = {𝑥 ∣ (𝐵 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}})})
12		df-op 3700	. 2 ⊢ ⟨𝐴, 𝐶⟩ = {𝑥 ∣ (𝐴 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}})}
13		df-op 3700	. 2 ⊢ ⟨𝐵, 𝐶⟩ = {𝑥 ∣ (𝐵 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}})}
14	11, 12, 13	3eqtr4g 2292	1 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 1005   = wceq 1398   ∈ wcel 2205  {cab 2220  Vcvv 2815  {csn 3691  {cpr 3692  ⟨cop 3694

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-un 3217  df-sn 3697  df-pr 3698  df-op 3700

This theorem is referenced by:  opeq12  3887  opeq1i  3888  opeq1d  3891  oteq1  3894  breq1  4114  cbvopab1  4185  cbvopab1s  4187  opthg  4356  eqvinop  4361  opelopabsb  4380  opelxp  4781  elvvv  4815  opabid2  4888  opeliunxp2  4897  elsnres  5077  elimasng  5132  rnxpid  5199  dmsnopg  5236  cnvsng  5250  elxp4  5252  elxp5  5253  funopg  5388  f1osng  5659  dmfco  5747  fvelrn  5810  fsng  5852  fvsng  5882  funfvima3  5922  oveq1  6059  oprabid  6084  dfoprab2  6102  cbvoprab1  6127  opabex3d  6316  opabex3  6317  op1stg  6346  op2ndg  6347  oprssdmm  6367  dfoprab4f  6389  cnvoprab  6432  opeliunxp2f  6471  tfr1onlemaccex  6581  tfrcllemaccex  6594  elixpsn  6972  fundmen  7049  xpsnen  7074  xpassen  7083  xpf1o  7099  ltexnqq  7725  archnqq  7734  prarloclemarch2  7736  prarloclemlo  7811  prarloclem3  7814  prarloclem5  7817  caucvgprlemnkj  7983  caucvgprlemnbj  7984  caucvgprlemm  7985  caucvgprlemdisj  7991  caucvgprlemloc  7992  caucvgprlemcl  7993  caucvgprlemladdfu  7994  caucvgprlemladdrl  7995  caucvgprlem1  7996  caucvgprlem2  7997  caucvgpr  7999  caucvgprprlemell  8002  caucvgprprlemelu  8003  caucvgprprlemcbv  8004  caucvgprprlemval  8005  caucvgprprlemnkeqj  8007  caucvgprprlemmu  8012  caucvgprprlemopl  8014  caucvgprprlemlol  8015  caucvgprprlemopu  8016  caucvgprprlemloc  8020  caucvgprprlemclphr  8022  caucvgprprlemexbt  8023  caucvgprprlem1  8026  caucvgprprlem2  8027  caucvgsr  8119  suplocsrlemb  8123  suplocsrlempr  8124  suplocsrlem  8125  suplocsr  8126  elrealeu  8146  pitonn  8165  nntopi  8211  axcaucvglemval  8214  axcaucvg  8217  axpre-suploclemres  8218  swrdccatin1  11421  swrdccat3blem  11435  fsum2dlemstep  12124  fprod2dlemstep  12312  imasaddfnlemg  13544  cnmpt21  15173