Theorem opeq1 3818

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 2267	. . . . . 6 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi1d 465	. . . . 5 ⊢ (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V)))
3		sneq 3643	. . . . . . 7 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
4		preq1 3709	. . . . . . 7 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
5	3, 4	preq12d 3717	. . . . . 6 ⊢ (𝐴 = 𝐵 → {{𝐴}, {𝐴, 𝐶}} = {{𝐵}, {𝐵, 𝐶}})
6	5	eleq2d 2274	. . . . 5 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ {{𝐴}, {𝐴, 𝐶}} ↔ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}}))
7	2, 6	anbi12d 473	. . . 4 ⊢ (𝐴 = 𝐵 → (((𝐴 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}}) ↔ ((𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}})))
8		df-3an 982	. . . 4 ⊢ ((𝐴 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}}) ↔ ((𝐴 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}}))
9		df-3an 982	. . . 4 ⊢ ((𝐵 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}}) ↔ ((𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}}))
10	7, 8, 9	3bitr4g 223	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}}) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}})))
11	10	abbidv 2322	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ (𝐴 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}})} = {𝑥 ∣ (𝐵 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}})})
12		df-op 3641	. 2 ⊢ ⟨𝐴, 𝐶⟩ = {𝑥 ∣ (𝐴 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐶}})}
13		df-op 3641	. 2 ⊢ ⟨𝐵, 𝐶⟩ = {𝑥 ∣ (𝐵 ∈ V ∧ 𝐶 ∈ V ∧ 𝑥 ∈ {{𝐵}, {𝐵, 𝐶}})}
14	11, 12, 13	3eqtr4g 2262	1 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 980   = wceq 1372   ∈ wcel 2175  {cab 2190  Vcvv 2771  {csn 3632  {cpr 3633  ⟨cop 3635

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 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-v 2773  df-un 3169  df-sn 3638  df-pr 3639  df-op 3641

This theorem is referenced by:  opeq12  3820  opeq1i  3821  opeq1d  3824  oteq1  3827  breq1  4046  cbvopab1  4116  cbvopab1s  4118  opthg  4281  eqvinop  4286  opelopabsb  4304  opelxp  4703  elvvv  4736  opabid2  4807  opeliunxp2  4816  elsnres  4993  elimasng  5047  rnxpid  5114  dmsnopg  5151  cnvsng  5165  elxp4  5167  elxp5  5168  funopg  5302  f1osng  5557  dmfco  5641  fvelrn  5705  fsng  5747  fvsng  5770  funfvima3  5808  oveq1  5941  oprabid  5966  dfoprab2  5982  cbvoprab1  6007  opabex3d  6196  opabex3  6197  op1stg  6226  op2ndg  6227  oprssdmm  6247  dfoprab4f  6269  cnvoprab  6310  opeliunxp2f  6314  tfr1onlemaccex  6424  tfrcllemaccex  6437  elixpsn  6812  fundmen  6883  xpsnen  6898  xpassen  6907  xpf1o  6923  ltexnqq  7503  archnqq  7512  prarloclemarch2  7514  prarloclemlo  7589  prarloclem3  7592  prarloclem5  7595  caucvgprlemnkj  7761  caucvgprlemnbj  7762  caucvgprlemm  7763  caucvgprlemdisj  7769  caucvgprlemloc  7770  caucvgprlemcl  7771  caucvgprlemladdfu  7772  caucvgprlemladdrl  7773  caucvgprlem1  7774  caucvgprlem2  7775  caucvgpr  7777  caucvgprprlemell  7780  caucvgprprlemelu  7781  caucvgprprlemcbv  7782  caucvgprprlemval  7783  caucvgprprlemnkeqj  7785  caucvgprprlemmu  7790  caucvgprprlemopl  7792  caucvgprprlemlol  7793  caucvgprprlemopu  7794  caucvgprprlemloc  7798  caucvgprprlemclphr  7800  caucvgprprlemexbt  7801  caucvgprprlem1  7804  caucvgprprlem2  7805  caucvgsr  7897  suplocsrlemb  7901  suplocsrlempr  7902  suplocsrlem  7903  suplocsr  7904  elrealeu  7924  pitonn  7943  nntopi  7989  axcaucvglemval  7992  axcaucvg  7995  axpre-suploclemres  7996  fsum2dlemstep  11664  fprod2dlemstep  11852  imasaddfnlemg  13064  cnmpt21  14681