Theorem opabbii 5164

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

Syntax hints:   ↔ wb 208   = wceq 1559  {copab 5159

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-opab 5160

This theorem is referenced by:  mptv  5203  2rbropap  5531  dfid4  5539  fconstmpt  5705  xpundi  5712  xpundir  5713  cnvi  5853  csbcnv  5854  csbcnvOLD  5855  cnvco  5857  resopab  6019  opabresid  6035  cnvun  6122  cnvxp  6138  cnvcnv3  6169  coundi  6229  coundir  6230  mptun  6662  fvopab6  7005  fmptsng  7147  fmptsnd  7148  cbvoprab1  7478  cbvoprab12  7480  dmoprabss  7495  mpomptx  7504  resoprab  7509  elrnmpores  7529  ov6g  7555  1st2val  7993  2nd2val  7994  dfoprab3s  8029  dfoprab3  8030  dfoprab4  8031  opabn1stprc  8034  mptmpoopabbrd  8056  fsplit  8090  mapsncnv  8869  xpcomco  9033  marypha2lem2  9376  oemapso  9631  ttrclresv  9666  leweon  9961  r0weon  9962  compsscnv  10322  fpwwe  10598  ltrelxr  11237  ltxrlt  11247  ltxr  13111  shftidt2  15088  prdsle  17482  prdsless  17483  prdsleval  17497  dfiso2  17796  joindm  18396  meetdm  18410  gaorb  19338  efgcpbllema  19785  frgpuplem  19803  dvdsrzring  21501  pjfval2  21749  ltbval  22084  ltbwe  22085  opsrle  22088  opsrtoslem1  22096  opsrtoslem2  22097  lmfval  23280  lmbr  23306  lgsquadlem3  27434  perpln1  28867  outpasch  28912  ishpg  28916  axcontlem2  29123  wksfval  29767  wlkson  29812  pthsfval  29876  ispth  29878  dfadj2  32045  dmadjss  32047  cnvadj  32052  mpomptxf  32841  lsmsnorb2  33539  satfv0  35669  satfvsuclem1  35670  satfvsuclem2  35671  satfbrsuc  35677  satf0  35683  satf0suclem  35686  fmlasuc0  35695  dfsuccf2  36252  fneer  36674  bj-dfmpoa  37569  bj-mpomptALT  37570  bj-brab2a1  37602  bj-imdiridlem  37638  bj-opabco  37641  opropabco  38184  xpv  38722  cnvepres  38764  inxp2  38835  disjecxrn  38872  xrninxp  38875  xrninxp2  38876  rnxrnres  38882  rnxrncnvepres  38883  rnxrnidres  38884  blockadjliftmap  38918  dfsucmap3  38923  dfsucmap4  38925  dfcoss2  38963  dfcoss3  38964  cosscnv  38966  coss1cnvres  38967  coss2cnvepres  38968  1cossres  38979  dfcoels  38980  ressn2  38992  br1cosscnvxrn  39024  1cosscnvxrn  39025  coss0  39029  cossid  39030  dfssr2  39039  dfpetparts2  39432  dfpeters2  39434  petseq  39436  cmtfvalN  39795  cmtvalN  39796  cvrfval  39853  cvrval  39854  dicval2  41764  aks6d1c1p1rcl  42686  aks6d1c1rh  42703  fgraphopab  43741  fgraphxp  43742  modelaxreplem2  45516  mptssid  45777  dfnelbr2  47828  opabbrfex0d  47841  opabbrfexd  47843  upwlksfval  48718  xpsnopab  48740  mpomptx2  48918  upfval2  49759