Theorem opabbii 4649

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

Hypothesis

Ref	Expression
opabbii.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
opabbii	⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜓}

Proof of Theorem opabbii

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2610	. 2 ⊢ 𝑧 = 𝑧
2		opabbii.1	. . . 4 ⊢ (𝜑 ↔ 𝜓)
3	2	a1i 11	. . 3 ⊢ (𝑧 = 𝑧 → (𝜑 ↔ 𝜓))
4	3	opabbidv 4648	. 2 ⊢ (𝑧 = 𝑧 → {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜓})
5	1, 4	ax-mp 5	1 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜓}

Syntax hints:   ↔ wb 195   = wceq 1475  {copab 4642

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-opab 4644

This theorem is referenced by:  mptv  4679  2rbropap  4941  dfid4  4955  fconstmpt  5085  xpundi  5094  xpundir  5095  inxp  5176  csbcnv  5228  cnvco  5230  resopab  5366  opabresid  5374  cnvi  5456  cnvun  5457  cnvxp  5470  cnvcnv3  5501  coundi  5553  coundir  5554  mptun  5938  fvopab6  6218  fmptsng  6339  fmptsnd  6340  fvmptopab2  6595  cbvoprab1  6625  cbvoprab12  6627  dmoprabss  6640  mpt2mptx  6649  resoprab  6654  elrnmpt2res  6672  ov6g  6696  1st2val  7085  2nd2val  7086  dfoprab3s  7114  dfoprab3  7115  dfoprab4  7116  fsplit  7169  mapsncnv  7790  xpcomco  7935  marypha2lem2  8225  oemapso  8462  leweon  8717  r0weon  8718  compsscnv  9076  fpwwe  9347  ltrelxr  9978  ltxrlt  9987  ltxr  11825  shftidt2  13669  prdsle  15945  prdsless  15946  prdsleval  15960  dfiso2  16255  joindm  16826  meetdm  16840  gaorb  17563  efgcpbllema  17990  frgpuplem  18008  ltbval  19292  ltbwe  19293  opsrle  19296  opsrtoslem1  19305  opsrtoslem2  19306  dvdsrzring  19650  pjfval2  19872  lmfval  20846  lmbr  20872  cnmptid  21274  lgsquadlem3  24907  perpln1  25405  outpasch  25447  ishpg  25451  axcontlem2  25645  wlks  26047  trls  26066  dfconngra1  26199  dfadj2  28128  dmadjss  28130  cnvadj  28135  mpt2mptxf  28860  fneer  31518  bj-dfmpt2a  32252  bj-mpt2mptALT  32253  opropabco  32688  cmtfvalN  33515  cmtvalN  33516  cvrfval  33573  cvrval  33574  dicval2  35486  fgraphopab  36807  fgraphxp  36808  opabn1stprc  40318  opabbrfex0d  40331  opabbrfexd  40333  mptmpt2opabbrd  40335  1wlksfval  40811  wlksfval  40812  wlkson  40864  xpsnopab  41555  mpt2mptx2  41906