Theorem opabbidv 5185

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 1924	. . 3 ⊢ (𝜑 → (∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜓) ↔ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜒)))
4	3	abbidv 2801	. 2 ⊢ (𝜑 → {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜓)} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜒)})
5		df-opab 5182	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜓} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜓)}
6		df-opab 5182	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜒} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜒)}
7	4, 5, 6	3eqtr4g 2795	1 ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜓} = {⟨𝑥, 𝑦⟩ ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540  ∃wex 1779  {cab 2713  ⟨cop 4607  {copab 5181

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 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-opab 5182

This theorem is referenced by:  opabbii  5186  mpteq12dva  5206  csbopab  5530  csbopabgALT  5531  csbmpt12  5532  xpeq1  5668  xpeq2  5675  opabbi2dv  5829  csbcnvgALT  5864  resopab2  6023  mptcnv  6128  cores  6238  xpco  6278  dffn5  6937  f1oiso2  7345  fvmptopab  7461  fvmptopabOLD  7462  f1ocnvd  7658  ofreq  7675  mptmpoopabbrd  8079  mptmpoopabbrdOLD  8080  mptmpoopabbrdOLDOLD  8082  bropopvvv  8089  bropfvvvv  8091  fnwelem  8130  sprmpod  8223  mpocurryd  8268  wemapwe  9711  ttrcleq  9723  xpcogend  14993  shftfval  15089  2shfti  15099  prdsval  17469  pwsle  17506  sectffval  17763  sectfval  17764  isfunc  17877  isfull  17925  isfth  17929  ipoval  18540  eqgfval  19159  eqg0subg  19179  dvdsrval  20321  dvdsrpropd  20376  ltbval  22001  opsrval  22004  lmfval  23170  xkocnv  23752  tgphaus  24055  isphtpc  24944  bcthlem1  25276  bcth  25281  dvcnp2  25873  dvmulbr  25893  dvcobr  25901  cmvth  25947  dvfsumle  25978  dvfsumlem2  25985  taylthlem2  26334  ulmval  26341  lgsquadlem3  27345  iscgrg  28491  legval  28563  ishlg  28581  perpln1  28689  perpln2  28690  isperp  28691  ishpg  28738  iscgra  28788  isinag  28817  isleag  28826  wksfval  29589  upgrtrls  29681  upgrspthswlk  29720  ajfval  30790  f1o3d  32605  f1od2  32698  mgcoval  32966  inftmrel  33178  isinftm  33179  erlval  33253  rlocval  33254  quslsm  33420  idlsrgval  33518  metidval  33921  faeval  34277  eulerpartlemgvv  34408  eulerpart  34414  afsval  34703  satf  35375  satfvsuc  35383  satfv1  35385  satf0suc  35398  sat1el2xp  35401  fmlasuc0  35406  bj-imdirvallem  37198  bj-imdirval2  37201  bj-imdirco  37208  bj-iminvval2  37212  cureq  37620  curf  37622  curunc  37626  fnopabeqd  37745  cosseq  38444  lcvfbr  39038  cmtfvalN  39228  cvrfval  39286  dicffval  41193  dicfval  41194  dicval  41195  prjspval  42626  prjspnerlem  42640  0prjspn  42651  dnwech  43072  aomclem8  43085  tfsconcatun  43361  tfsconcat0i  43369  tfsconcatrev  43372  rfovcnvfvd  44031  fsovrfovd  44033  dfafn5a  47189  sprsymrelfv  47508  sprsymrelfo  47511  upwlksfval  48110  sectpropdlem  49003  upfval  49111  upfval2  49112  upfval3  49113