Theorem opabbidv 5232

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537  ∃wex 1777  {cab 2717  ⟨cop 4654  {copab 5228

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-opab 5229

This theorem is referenced by:  opabbii  5233  mpteq12dva  5255  csbopab  5574  csbopabgALT  5575  csbmpt12  5576  xpeq1  5714  xpeq2  5721  opabbi2dv  5874  csbcnvgALT  5909  resopab2  6065  mptcnv  6171  cores  6280  xpco  6320  dffn5  6980  f1oiso2  7388  fvmptopab  7504  fvmptopabOLD  7505  f1ocnvd  7701  ofreq  7718  mptmpoopabbrd  8121  mptmpoopabbrdOLD  8122  mptmpoopabbrdOLDOLD  8124  bropopvvv  8131  bropfvvvv  8133  fnwelem  8172  sprmpod  8265  mpocurryd  8310  wemapwe  9766  ttrcleq  9778  xpcogend  15023  shftfval  15119  2shfti  15129  prdsval  17515  pwsle  17552  sectffval  17811  sectfval  17812  isfunc  17928  isfull  17977  isfth  17981  ipoval  18600  eqgfval  19216  eqg0subg  19236  dvdsrval  20387  dvdsrpropd  20442  ltbval  22084  opsrval  22087  lmfval  23261  xkocnv  23843  tgphaus  24146  isphtpc  25045  bcthlem1  25377  bcth  25382  dvcnp2  25975  dvmulbr  25995  dvcobr  26003  cmvth  26049  dvfsumle  26080  dvfsumlem2  26087  taylthlem2  26434  ulmval  26441  lgsquadlem3  27444  iscgrg  28538  legval  28610  ishlg  28628  perpln1  28736  perpln2  28737  isperp  28738  ishpg  28785  iscgra  28835  isinag  28864  isleag  28873  wksfval  29645  upgrtrls  29737  upgrspthswlk  29774  ajfval  30841  f1o3d  32646  f1od2  32735  mgcoval  32959  inftmrel  33160  isinftm  33161  erlval  33230  rlocval  33231  quslsm  33398  idlsrgval  33496  metidval  33836  faeval  34210  eulerpartlemgvv  34341  eulerpart  34347  afsval  34648  satf  35321  satfvsuc  35329  satfv1  35331  satf0suc  35344  sat1el2xp  35347  fmlasuc0  35352  bj-imdirvallem  37146  bj-imdirval2  37149  bj-imdirco  37156  bj-iminvval2  37160  cureq  37556  curf  37558  curunc  37562  fnopabeqd  37681  cosseq  38382  lcvfbr  38976  cmtfvalN  39166  cvrfval  39224  dicffval  41131  dicfval  41132  dicval  41133  prjspval  42558  prjspnerlem  42572  0prjspn  42583  dnwech  43005  aomclem8  43018  tfsconcatun  43299  tfsconcat0i  43307  tfsconcatrev  43310  rfovcnvfvd  43969  fsovrfovd  43971  dfafn5a  47075  sprsymrelfv  47368  sprsymrelfo  47371  upwlksfval  47858