Theorem opabbii 5180

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

Syntax hints:   ↔ wb 209   = wceq 1567  {copab 5175

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-opab 5176

This theorem is referenced by:  mptv  5219  2rbropap  5550  dfid4  5558  fconstmpt  5724  xpundi  5731  xpundir  5732  cnvi  5872  csbcnv  5873  csbcnvOLD  5874  cnvco  5876  resopab  6037  opabresid  6053  cnvun  6140  cnvxp  6155  cnvcnv3  6187  coundi  6249  coundir  6250  mptun  6682  fvopab6  7025  fmptsng  7167  fmptsnd  7168  cbvoprab1  7498  cbvoprab12  7500  dmoprabss  7515  mpomptx  7524  resoprab  7529  elrnmpores  7549  ov6g  7575  1st2val  8014  2nd2val  8015  dfoprab3s  8050  dfoprab3  8051  dfoprab4  8052  opabn1stprc  8055  mptmpoopabbrd  8078  fsplit  8112  mapsncnv  8891  xpcomco  9055  marypha2lem2  9396  oemapso  9651  ttrclresv  9686  leweon  9995  r0weon  9996  compsscnv  10355  fpwwe  10631  ltrelxr  11270  ltxrlt  11280  ltxr  13140  shftidt2  15118  prdsle  17515  prdsless  17516  prdsleval  17530  dfiso2  17829  joindm  18429  meetdm  18443  gaorb  19377  efgcpbllema  19824  frgpuplem  19842  dvdsrzring  21580  pjfval2  21828  ltbval  22163  ltbwe  22164  opsrle  22167  opsrtoslem1  22175  opsrtoslem2  22176  lmfval  23358  lmbr  23384  lgsquadlem3  27512  perpln1  28949  outpasch  28996  ishpg  29000  axcontlem2  29256  wksfval  29900  wlkson  29945  pthsfval  30009  ispth  30011  dfadj2  32178  dmadjss  32180  cnvadj  32185  mpomptxf  32964  lsmsnorb2  33649  satfv0  35783  satfvsuclem1  35784  satfvsuclem2  35785  satfbrsuc  35791  satf0  35797  satf0suclem  35800  fmlasuc0  35809  dfsuccf2  36366  fneer  36787  bj-dfmpoa  37683  bj-mpomptALT  37684  bj-brab2a1  37716  bj-imdiridlem  37752  bj-opabco  37755  opropabco  38298  xpv  38836  cnvepres  38878  inxp2  38949  disjecxrn  38986  xrninxp  38989  xrninxp2  38990  rnxrnres  38996  rnxrncnvepres  38997  rnxrnidres  38998  blockadjliftmap  39032  dfsucmap3  39037  dfsucmap4  39039  dfcoss2  39077  dfcoss3  39078  cosscnv  39080  coss1cnvres  39081  coss2cnvepres  39082  1cossres  39093  dfcoels  39094  ressn2  39106  br1cosscnvxrn  39138  1cosscnvxrn  39139  coss0  39143  cossid  39144  dfssr2  39153  dfpetparts2  39546  dfpeters2  39548  petseq  39550  cmtfvalN  39909  cmtvalN  39910  cvrfval  39967  cvrval  39968  dicval2  41878  aks6d1c1p1rcl  42800  aks6d1c1rh  42817  fgraphopab  43857  fgraphxp  43858  modelaxreplem2  45615  mptssid  45883  dfnelbr2  47934  opabbrfex0d  47947  opabbrfexd  47949  upwlksfval  48824  xpsnopab  48846  mpomptx2  49035  upfval2  49875