Theorem opabbii 5153

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

Syntax hints:   ↔ wb 206   = wceq 1541  {copab 5148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-opab 5149

This theorem is referenced by:  mptv  5192  2rbropap  5499  dfid4  5507  fconstmpt  5673  xpundi  5680  xpundir  5681  inxpOLD  5767  csbcnv  5818  cnvco  5820  resopab  5978  opabresid  5994  cnvi  6083  cnvun  6084  cnvxp  6099  cnvcnv3  6130  coundi  6189  coundir  6190  mptun  6622  fvopab6  6958  fmptsng  7097  fmptsnd  7098  cbvoprab1  7428  cbvoprab12  7430  dmoprabss  7445  mpomptx  7454  resoprab  7459  elrnmpores  7479  ov6g  7505  1st2val  7944  2nd2val  7945  dfoprab3s  7980  dfoprab3  7981  dfoprab4  7982  opabn1stprc  7985  mptmpoopabbrd  8007  mptmpoopabbrdOLD  8008  fsplit  8042  mapsncnv  8812  xpcomco  8975  marypha2lem2  9315  oemapso  9567  ttrclresv  9602  leweon  9897  r0weon  9898  compsscnv  10257  fpwwe  10532  ltrelxr  11168  ltxrlt  11178  ltxr  13009  shftidt2  14983  prdsle  17361  prdsless  17362  prdsleval  17376  dfiso2  17674  joindm  18274  meetdm  18288  gaorb  19214  efgcpbllema  19661  frgpuplem  19679  dvdsrzring  21393  pjfval2  21641  ltbval  21973  ltbwe  21974  opsrle  21977  opsrtoslem1  21985  opsrtoslem2  21986  lmfval  23142  lmbr  23168  lgsquadlem3  27315  perpln1  28683  outpasch  28728  ishpg  28732  axcontlem2  28938  wksfval  29583  wlkson  29628  pthsfval  29692  ispth  29694  dfadj2  31857  dmadjss  31859  cnvadj  31864  mpomptxf  32651  lsmsnorb2  33349  satfv0  35394  satfvsuclem1  35395  satfvsuclem2  35396  satfbrsuc  35402  satf0  35408  satf0suclem  35411  fmlasuc0  35420  fneer  36387  bj-dfmpoa  37152  bj-mpomptALT  37153  bj-brab2a1  37183  bj-imdiridlem  37219  bj-opabco  37222  opropabco  37764  cnvepres  38332  inxp2  38395  disjecxrn  38421  xrninxp  38424  xrninxp2  38425  rnxrnres  38431  rnxrncnvepres  38432  rnxrnidres  38433  dfcoss2  38450  dfcoss3  38451  cosscnv  38453  coss1cnvres  38454  coss2cnvepres  38455  1cossres  38466  dfcoels  38467  ressn2  38479  br1cosscnvxrn  38511  1cosscnvxrn  38512  coss0  38516  cossid  38517  dfssr2  38536  cmtfvalN  39249  cmtvalN  39250  cvrfval  39307  cvrval  39308  dicval2  41218  aks6d1c1p1rcl  42141  aks6d1c1rh  42158  fgraphopab  43236  fgraphxp  43237  modelaxreplem2  45012  mptssid  45278  dfnelbr2  47304  opabbrfex0d  47317  opabbrfexd  47319  upwlksfval  48166  xpsnopab  48188  mpomptx2  48366  upfval2  49209