Theorem opeq1 3644

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 2157	. . . . . 6 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi1d 454	. . . . 5 ⊢ (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V)))
3		sneq 3477	. . . . . . 7 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
4		preq1 3539	. . . . . . 7 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
5	3, 4	preq12d 3547	. . . . . 6 ⊢ (𝐴 = 𝐵 → {{𝐴}, {𝐴, 𝐶}} = {{𝐵}, {𝐵, 𝐶}})
6	5	eleq2d 2164	. . . . 5 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ {{𝐴}, {𝐴, 𝐶}} ↔ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}}))
7	2, 6	anbi12d 458	. . . 4 ⊢ (𝐴 = 𝐵 → (((𝐴 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}}) ↔ ((𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}})))
8		df-3an 929	. . . 4 ⊢ ((𝐴 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}}) ↔ ((𝐴 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}}))
9		df-3an 929	. . . 4 ⊢ ((𝐵 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}}) ↔ ((𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}}))
10	7, 8, 9	3bitr4g 222	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}}) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}})))
11	10	abbidv 2212	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ (𝐴 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}})} = {𝑥 ∣ (𝐵 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}})})
12		df-op 3475	. 2 ⊢ ⟨𝐴, 𝐶⟩ = {𝑥 ∣ (𝐴 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}})}
13		df-op 3475	. 2 ⊢ ⟨𝐵, 𝐶⟩ = {𝑥 ∣ (𝐵 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}})}
14	11, 12, 13	3eqtr4g 2152	1 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 927   = wceq 1296   ∈ wcel 1445  {cab 2081  Vcvv 2633  {csn 3466  {cpr 3467  ⟨cop 3469

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077

This theorem depends on definitions:  df-bi 116  df-3an 929  df-tru 1299  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-v 2635  df-un 3017  df-sn 3472  df-pr 3473  df-op 3475

This theorem is referenced by:  opeq12  3646  opeq1i  3647  opeq1d  3650  oteq1  3653  breq1  3870  cbvopab1  3933  cbvopab1s  3935  opthg  4089  eqvinop  4094  opelopabsb  4111  opelxp  4497  elvvv  4530  opabid2  4598  opeliunxp2  4607  elsnres  4782  elimasng  4833  rnxpid  4899  dmsnopg  4936  cnvsng  4950  elxp4  4952  elxp5  4953  funopg  5082  f1osng  5329  dmfco  5407  fvelrn  5469  fsng  5509  fvsng  5532  funfvima3  5567  oveq1  5697  oprabid  5719  dfoprab2  5734  cbvoprab1  5758  opabex3d  5930  opabex3  5931  op1stg  5959  op2ndg  5960  dfoprab4f  6001  cnvoprab  6037  opeliunxp2f  6041  tfr1onlemaccex  6151  tfrcllemaccex  6164  elixpsn  6532  fundmen  6603  xpsnen  6617  xpassen  6626  xpf1o  6640  djur  6837  ltexnqq  7064  archnqq  7073  prarloclemarch2  7075  prarloclemlo  7150  prarloclem3  7153  prarloclem5  7156  caucvgprlemnkj  7322  caucvgprlemnbj  7323  caucvgprlemm  7324  caucvgprlemdisj  7330  caucvgprlemloc  7331  caucvgprlemcl  7332  caucvgprlemladdfu  7333  caucvgprlemladdrl  7334  caucvgprlem1  7335  caucvgprlem2  7336  caucvgpr  7338  caucvgprprlemell  7341  caucvgprprlemelu  7342  caucvgprprlemcbv  7343  caucvgprprlemval  7344  caucvgprprlemnkeqj  7346  caucvgprprlemmu  7351  caucvgprprlemopl  7353  caucvgprprlemlol  7354  caucvgprprlemopu  7355  caucvgprprlemloc  7359  caucvgprprlemclphr  7361  caucvgprprlemexbt  7362  caucvgprprlem1  7365  caucvgprprlem2  7366  caucvgsr  7444  elrealeu  7464  pitonn  7482  nntopi  7526  axcaucvglemval  7529  axcaucvg  7532  fsum2dlemstep  10993