Theorem opabbii 4922

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 2817	. 2 ⊢ 𝑧 = 𝑧
2		opabbii.1	. . . 4 ⊢ (𝜑 ↔ 𝜓)
3	2	a1i 11	. . 3 ⊢ (𝑧 = 𝑧 → (𝜑 ↔ 𝜓))
4	3	opabbidv 4921	. 2 ⊢ (𝑧 = 𝑧 → {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜓})
5	1, 4	ax-mp 5	1 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜓}

Syntax hints:   ↔ wb 197   = wceq 1637  {copab 4917

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-ext 2795

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-opab 4918

This theorem is referenced by:  mptv  4956  2rbropap  5225  dfid4  5234  fconstmpt  5376  xpundi  5384  xpundir  5385  inxp  5469  csbcnv  5520  cnvco  5522  resopab  5664  opabresid  5680  cnvi  5761  cnvun  5762  cnvxp  5775  cnvcnv3  5806  coundi  5863  coundir  5864  mptun  6245  fvopab6  6541  fmptsng  6668  fmptsnd  6669  cbvoprab1  6966  cbvoprab12  6968  dmoprabss  6981  mpt2mptx  6990  resoprab  6995  elrnmpt2res  7013  ov6g  7037  1st2val  7435  2nd2val  7436  dfoprab3s  7464  dfoprab3  7465  dfoprab4  7466  opabn1stprc  7469  mptmpt2opabbrd  7490  fsplit  7525  mapsncnv  8150  xpcomco  8298  marypha2lem2  8590  oemapso  8835  leweon  9126  r0weon  9127  compsscnv  9487  fpwwe  9762  ltrelxr  10393  ltxrlt  10402  ltxr  12184  shftidt2  14063  prdsle  16346  prdsless  16347  prdsleval  16361  dfiso2  16655  joindm  17227  meetdm  17241  gaorb  17960  efgcpbllema  18387  frgpuplem  18405  ltbval  19699  ltbwe  19700  opsrle  19703  opsrtoslem1  19711  opsrtoslem2  19712  dvdsrzring  20058  pjfval2  20283  lmfval  21270  lmbr  21296  cnmptid  21698  lgsquadlem3  25343  perpln1  25841  outpasch  25883  ishpg  25887  axcontlem2  26081  wksfval  26755  wlkson  26802  pthsfval  26867  ispth  26869  dfadj2  29094  dmadjss  29096  cnvadj  29101  mpt2mptxf  29826  fneer  32690  bj-dfmpt2a  33400  bj-mpt2mptALT  33401  cnfinltrel  33575  opropabco  33848  cnvepres  34401  inxp2  34460  xrninxp  34481  xrninxp2  34482  rnxrnres  34488  rnxrncnvepres  34489  rnxrnidres  34490  dfcoss2  34502  dfcoss3  34503  1cossres  34515  dfcoels  34516  br1cosscnvxrn  34555  1cosscnvxrn  34556  coss0  34560  cossid  34561  dfssr2  34580  cmtfvalN  35008  cmtvalN  35009  cvrfval  35066  cvrval  35067  dicval2  36977  fgraphopab  38306  fgraphxp  38307  dfnelbr2  41879  opabbrfex0d  41893  opabbrfexd  41895  upwlksfval  42301  xpsnopab  42350  mpt2mptx2  42698