Theorem opabbidv 5213

Description: Equivalent wff's yield equal ordered-pair class abstractions (deduction form). (Contributed by NM, 15-May-1995.)

Hypothesis

Ref	Expression
opabbidv.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
opabbidv	⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜓} = {⟨𝑥, 𝑦⟩ ∣ 𝜒})

Distinct variable groups:   𝜑,𝑥   𝜑,𝑦

Allowed substitution hints:   𝜓(𝑥,𝑦)   𝜒(𝑥,𝑦)

Proof of Theorem opabbidv

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		opabbidv.1	. . . . 5 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	anbi2d 627	. . . 4 ⊢ (𝜑 → ((𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜓) ↔ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜒)))
3	2	2exbidv 1925	. . 3 ⊢ (𝜑 → (∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜓) ↔ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜒)))
4	3	abbidv 2799	. 2 ⊢ (𝜑 → {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜓)} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜒)})
5		df-opab 5210	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜓} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜓)}
6		df-opab 5210	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜒} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜒)}
7	4, 5, 6	3eqtr4g 2795	1 ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜓} = {⟨𝑥, 𝑦⟩ ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   = wceq 1539  ∃wex 1779  {cab 2707  ⟨cop 4633  {copab 5209

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-opab 5210

This theorem is referenced by:  opabbii  5214  mpteq12dva  5236  csbopab  5554  csbopabgALT  5555  csbmpt12  5556  xpeq1  5689  xpeq2  5696  opabbi2dv  5848  csbcnvgALT  5883  resopab2  6035  mptcnv  6138  cores  6247  xpco  6287  dffn5  6949  f1oiso2  7351  fvmptopab  7465  fvmptopabOLD  7466  f1ocnvd  7659  ofreq  7676  mptmpoopabbrd  8069  mptmpoopabbrdOLD  8071  bropopvvv  8078  bropfvvvv  8080  fnwelem  8119  sprmpod  8211  mpocurryd  8256  wemapwe  9694  ttrcleq  9706  xpcogend  14925  shftfval  15021  2shfti  15031  prdsval  17405  pwsle  17442  sectffval  17701  sectfval  17702  isfunc  17818  isfull  17865  isfth  17869  ipoval  18487  eqgfval  19092  eqg0subg  19111  dvdsrval  20252  dvdsrpropd  20307  ltbval  21817  opsrval  21820  lmfval  22956  xkocnv  23538  tgphaus  23841  isphtpc  24740  bcthlem1  25072  bcth  25077  dvcnp2  25669  dvmulbr  25689  dvcobr  25697  ulmval  26128  lgsquadlem3  27121  iscgrg  28030  legval  28102  ishlg  28120  perpln1  28228  perpln2  28229  isperp  28230  ishpg  28277  iscgra  28327  isinag  28356  isleag  28365  wksfval  29133  upgrtrls  29225  upgrspthswlk  29262  ajfval  30329  f1o3d  32118  f1od2  32213  mgcoval  32423  inftmrel  32596  isinftm  32597  quslsm  32790  idlsrgval  32891  metidval  33168  faeval  33542  eulerpartlemgvv  33673  eulerpart  33679  afsval  33981  satf  34642  satfvsuc  34650  satfv1  34652  satf0suc  34665  sat1el2xp  34668  fmlasuc0  34673  gg-cmvth  35466  gg-dvfsumle  35468  gg-dvfsumlem2  35469  bj-imdirvallem  36364  bj-imdirval2  36367  bj-imdirco  36374  bj-iminvval2  36378  cureq  36767  curf  36769  curunc  36773  fnopabeqd  36892  cosseq  37599  lcvfbr  38193  cmtfvalN  38383  cvrfval  38441  dicffval  40348  dicfval  40349  dicval  40350  prjspval  41647  prjspnerlem  41661  0prjspn  41672  dnwech  42092  aomclem8  42105  tfsconcatun  42389  tfsconcat0i  42397  tfsconcatrev  42400  rfovcnvfvd  43060  fsovrfovd  43062  dfafn5a  46166  sprsymrelfv  46460  sprsymrelfo  46463  upwlksfval  46811