Theorem opabbidv 5157

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 630	. . . 4 ⊢ (𝜑 → ((𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜓) ↔ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜒)))
3	2	2exbidv 1925	. . 3 ⊢ (𝜑 → (∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜓) ↔ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜒)))
4	3	abbidv 2797	. 2 ⊢ (𝜑 → {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜓)} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜒)})
5		df-opab 5154	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜓} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜓)}
6		df-opab 5154	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜒} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜒)}
7	4, 5, 6	3eqtr4g 2791	1 ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜓} = {⟨𝑥, 𝑦⟩ ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541  ∃wex 1780  {cab 2709  ⟨cop 4582  {copab 5153

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-opab 5154

This theorem is referenced by:  opabbii  5158  mpteq12dva  5177  csbopab  5495  csbopabgALT  5496  csbmpt12  5497  xpeq1  5630  xpeq2  5637  opabbi2dv  5789  csbcnvgALT  5824  resopab2  5985  mptcnv  6086  cores  6196  xpco  6236  dffn5  6880  f1oiso2  7286  fvmptopab  7401  f1ocnvd  7597  ofreq  7614  mptmpoopabbrd  8012  mptmpoopabbrdOLD  8013  bropopvvv  8020  bropfvvvv  8022  fnwelem  8061  sprmpod  8154  mpocurryd  8199  wemapwe  9587  ttrcleq  9599  xpcogend  14878  shftfval  14974  2shfti  14984  prdsval  17356  pwsle  17393  sectffval  17654  sectfval  17655  isfunc  17768  isfull  17816  isfth  17820  ipoval  18433  eqgfval  19086  eqg0subg  19106  dvdsrval  20277  dvdsrpropd  20332  ltbval  21976  opsrval  21979  lmfval  23145  xkocnv  23727  tgphaus  24030  isphtpc  24918  bcthlem1  25249  bcth  25254  dvcnp2  25846  dvmulbr  25866  dvcobr  25874  cmvth  25920  dvfsumle  25951  dvfsumlem2  25958  taylthlem2  26307  ulmval  26314  lgsquadlem3  27318  iscgrg  28488  legval  28560  ishlg  28578  perpln1  28686  perpln2  28687  isperp  28688  ishpg  28735  iscgra  28785  isinag  28814  isleag  28823  wksfval  29586  upgrtrls  29676  upgrspthswlk  29714  ajfval  30784  f1o3d  32603  f1od2  32697  mgcoval  32962  inftmrel  33144  isinftm  33145  erlval  33220  rlocval  33221  quslsm  33365  idlsrgval  33463  metidval  33898  faeval  34254  eulerpartlemgvv  34384  eulerpart  34390  afsval  34679  satf  35385  satfvsuc  35393  satfv1  35395  satf0suc  35408  sat1el2xp  35411  fmlasuc0  35416  bj-imdirvallem  37213  bj-imdirval2  37216  bj-imdirco  37223  bj-iminvval2  37227  cureq  37635  curf  37637  curunc  37641  fnopabeqd  37760  cosseq  38462  lcvfbr  39058  cmtfvalN  39248  cvrfval  39306  dicffval  41212  dicfval  41213  dicval  41214  prjspval  42635  prjspnerlem  42649  0prjspn  42660  dnwech  43080  aomclem8  43093  tfsconcatun  43369  tfsconcat0i  43377  tfsconcatrev  43380  rfovcnvfvd  44039  fsovrfovd  44041  dfafn5a  47190  sprsymrelfv  47524  sprsymrelfo  47527  upwlksfval  48165  sectpropdlem  49067  upfval  49207  upfval2  49208  upfval3  49209  uppropd  49212