Theorem opeq1 3825

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 2269	. . . . . 6 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi1d 465	. . . . 5 ⊢ (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V)))
3		sneq 3649	. . . . . . 7 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
4		preq1 3715	. . . . . . 7 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
5	3, 4	preq12d 3723	. . . . . 6 ⊢ (𝐴 = 𝐵 → {{𝐴}, {𝐴, 𝐶}} = {{𝐵}, {𝐵, 𝐶}})
6	5	eleq2d 2276	. . . . 5 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ {{𝐴}, {𝐴, 𝐶}} ↔ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}}))
7	2, 6	anbi12d 473	. . . 4 ⊢ (𝐴 = 𝐵 → (((𝐴 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}}) ↔ ((𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}})))
8		df-3an 983	. . . 4 ⊢ ((𝐴 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}}) ↔ ((𝐴 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}}))
9		df-3an 983	. . . 4 ⊢ ((𝐵 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}}) ↔ ((𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}}))
10	7, 8, 9	3bitr4g 223	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}}) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}})))
11	10	abbidv 2324	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ (𝐴 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}})} = {𝑥 ∣ (𝐵 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}})})
12		df-op 3647	. 2 ⊢ ⟨𝐴, 𝐶⟩ = {𝑥 ∣ (𝐴 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}})}
13		df-op 3647	. 2 ⊢ ⟨𝐵, 𝐶⟩ = {𝑥 ∣ (𝐵 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}})}
14	11, 12, 13	3eqtr4g 2264	1 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 981   = wceq 1373   ∈ wcel 2177  {cab 2192  Vcvv 2773  {csn 3638  {cpr 3639  ⟨cop 3641

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-v 2775  df-un 3174  df-sn 3644  df-pr 3645  df-op 3647

This theorem is referenced by:  opeq12  3827  opeq1i  3828  opeq1d  3831  oteq1  3834  breq1  4054  cbvopab1  4125  cbvopab1s  4127  opthg  4290  eqvinop  4295  opelopabsb  4314  opelxp  4713  elvvv  4746  opabid2  4817  opeliunxp2  4826  elsnres  5005  elimasng  5059  rnxpid  5126  dmsnopg  5163  cnvsng  5177  elxp4  5179  elxp5  5180  funopg  5314  f1osng  5576  dmfco  5660  fvelrn  5724  fsng  5766  fvsng  5793  funfvima3  5831  oveq1  5964  oprabid  5989  dfoprab2  6005  cbvoprab1  6030  opabex3d  6219  opabex3  6220  op1stg  6249  op2ndg  6250  oprssdmm  6270  dfoprab4f  6292  cnvoprab  6333  opeliunxp2f  6337  tfr1onlemaccex  6447  tfrcllemaccex  6460  elixpsn  6835  fundmen  6912  xpsnen  6931  xpassen  6940  xpf1o  6956  ltexnqq  7541  archnqq  7550  prarloclemarch2  7552  prarloclemlo  7627  prarloclem3  7630  prarloclem5  7633  caucvgprlemnkj  7799  caucvgprlemnbj  7800  caucvgprlemm  7801  caucvgprlemdisj  7807  caucvgprlemloc  7808  caucvgprlemcl  7809  caucvgprlemladdfu  7810  caucvgprlemladdrl  7811  caucvgprlem1  7812  caucvgprlem2  7813  caucvgpr  7815  caucvgprprlemell  7818  caucvgprprlemelu  7819  caucvgprprlemcbv  7820  caucvgprprlemval  7821  caucvgprprlemnkeqj  7823  caucvgprprlemmu  7828  caucvgprprlemopl  7830  caucvgprprlemlol  7831  caucvgprprlemopu  7832  caucvgprprlemloc  7836  caucvgprprlemclphr  7838  caucvgprprlemexbt  7839  caucvgprprlem1  7842  caucvgprprlem2  7843  caucvgsr  7935  suplocsrlemb  7939  suplocsrlempr  7940  suplocsrlem  7941  suplocsr  7942  elrealeu  7962  pitonn  7981  nntopi  8027  axcaucvglemval  8030  axcaucvg  8033  axpre-suploclemres  8034  fsum2dlemstep  11820  fprod2dlemstep  12008  imasaddfnlemg  13221  cnmpt21  14838