Theorem opabbii 4942

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

Syntax hints:   ↔ wb 198   = wceq 1656  {copab 4937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-opab 4938

This theorem is referenced by:  mptv  4976  2rbropap  5245  dfid4  5254  fconstmpt  5402  xpundi  5408  xpundir  5409  inxp  5491  csbcnv  5542  cnvco  5544  resopab  5687  opabresid  5702  cnvi  5782  cnvun  5783  cnvxp  5796  cnvcnv3  5827  coundi  5881  coundir  5882  mptun  6262  fvopab6  6564  fmptsng  6691  fmptsnd  6692  cbvoprab1  6992  cbvoprab12  6994  dmoprabss  7007  mpt2mptx  7016  resoprab  7021  elrnmpt2res  7039  ov6g  7063  1st2val  7461  2nd2val  7462  dfoprab3s  7490  dfoprab3  7491  dfoprab4  7492  opabn1stprc  7495  mptmpt2opabbrd  7516  fsplit  7551  mapsncnv  8177  xpcomco  8325  marypha2lem2  8617  oemapso  8863  leweon  9154  r0weon  9155  compsscnv  9515  fpwwe  9790  ltrelxr  10425  ltxrlt  10434  ltxr  12242  shftidt2  14205  prdsle  16482  prdsless  16483  prdsleval  16497  dfiso2  16791  joindm  17363  meetdm  17377  gaorb  18097  efgcpbllema  18527  frgpuplem  18545  ltbval  19839  ltbwe  19840  opsrle  19843  opsrtoslem1  19851  opsrtoslem2  19852  dvdsrzring  20198  pjfval2  20423  lmfval  21414  lmbr  21440  cnmptid  21842  lgsquadlem3  25527  perpln1  26029  outpasch  26071  ishpg  26075  axcontlem2  26271  wksfval  26914  wlkson  26960  pthsfval  27030  ispth  27032  dfadj2  29295  dmadjss  29297  cnvadj  29302  mpt2mptxf  30021  fneer  32881  bj-dfmpt2a  33589  bj-mpt2mptALT  33590  cnfinltrel  33781  opropabco  34056  cnvepres  34612  inxp2  34672  xrninxp  34693  xrninxp2  34694  rnxrnres  34700  rnxrncnvepres  34701  rnxrnidres  34702  dfcoss2  34714  dfcoss3  34715  1cossres  34727  dfcoels  34728  br1cosscnvxrn  34767  1cosscnvxrn  34768  coss0  34772  cossid  34773  dfssr2  34792  cmtfvalN  35280  cmtvalN  35281  cvrfval  35338  cvrval  35339  dicval2  37249  fgraphopab  38626  fgraphxp  38627  dfnelbr2  42169  opabbrfex0d  42183  opabbrfexd  42185  upwlksfval  42577  xpsnopab  42626  mpt2mptx2  42974