Theorem opabbii 4717

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

Syntax hints:   ↔ wb 196   = wceq 1483  {copab 4712

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-opab 4713

This theorem is referenced by:  mptv  4751  2rbropap  5017  dfid4  5026  fconstmpt  5163  xpundi  5171  xpundir  5172  inxp  5254  csbcnv  5306  cnvco  5308  resopab  5446  opabresid  5455  cnvi  5537  cnvun  5538  cnvxp  5551  cnvcnv3  5582  coundi  5636  coundir  5637  mptun  6025  fvopab6  6310  fmptsng  6434  fmptsnd  6435  cbvoprab1  6727  cbvoprab12  6729  dmoprabss  6742  mpt2mptx  6751  resoprab  6756  elrnmpt2res  6774  ov6g  6798  1st2val  7194  2nd2val  7195  dfoprab3s  7223  dfoprab3  7224  dfoprab4  7225  opabn1stprc  7228  mptmpt2opabbrd  7248  fsplit  7282  mapsncnv  7904  xpcomco  8050  marypha2lem2  8342  oemapso  8579  leweon  8834  r0weon  8835  compsscnv  9193  fpwwe  9468  ltrelxr  10099  ltxrlt  10108  ltxr  11949  shftidt2  13821  prdsle  16122  prdsless  16123  prdsleval  16137  dfiso2  16432  joindm  17003  meetdm  17017  gaorb  17740  efgcpbllema  18167  frgpuplem  18185  ltbval  19471  ltbwe  19472  opsrle  19475  opsrtoslem1  19484  opsrtoslem2  19485  dvdsrzring  19831  pjfval2  20053  lmfval  21036  lmbr  21062  cnmptid  21464  lgsquadlem3  25107  perpln1  25605  outpasch  25647  ishpg  25651  axcontlem2  25845  wksfval  26505  wlkson  26552  pthsfval  26617  ispth  26619  dfadj2  28744  dmadjss  28746  cnvadj  28751  mpt2mptxf  29477  fneer  32348  bj-dfmpt2a  33071  bj-mpt2mptALT  33072  opropabco  33518  cnvepres  34066  inxp2  34129  cmtfvalN  34497  cmtvalN  34498  cvrfval  34555  cvrval  34556  dicval2  36468  fgraphopab  37788  fgraphxp  37789  dfnelbr2  41290  opabbrfex0d  41305  opabbrfexd  41307  upwlksfval  41716  xpsnopab  41765  mpt2mptx2  42113