Theorem opabbii 5177

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

Syntax hints:   ↔ wb 206   = wceq 1540  {copab 5172

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-opab 5173

This theorem is referenced by:  mptv  5216  2rbropap  5529  dfid4  5537  fconstmpt  5703  xpundi  5710  xpundir  5711  inxpOLD  5799  csbcnv  5850  cnvco  5852  resopab  6008  opabresid  6024  cnvi  6117  cnvun  6118  cnvxp  6133  cnvcnv3  6164  coundi  6223  coundir  6224  mptun  6667  fvopab6  7005  fmptsng  7145  fmptsnd  7146  cbvoprab1  7479  cbvoprab12  7481  dmoprabss  7496  mpomptx  7505  resoprab  7510  elrnmpores  7530  ov6g  7556  1st2val  7999  2nd2val  8000  dfoprab3s  8035  dfoprab3  8036  dfoprab4  8037  opabn1stprc  8040  mptmpoopabbrd  8062  mptmpoopabbrdOLD  8063  mptmpoopabbrdOLDOLD  8065  fsplit  8099  mapsncnv  8869  xpcomco  9036  marypha2lem2  9394  oemapso  9642  ttrclresv  9677  leweon  9971  r0weon  9972  compsscnv  10331  fpwwe  10606  ltrelxr  11242  ltxrlt  11251  ltxr  13082  shftidt2  15054  prdsle  17432  prdsless  17433  prdsleval  17447  dfiso2  17741  joindm  18341  meetdm  18355  gaorb  19246  efgcpbllema  19691  frgpuplem  19709  dvdsrzring  21378  pjfval2  21625  ltbval  21957  ltbwe  21958  opsrle  21961  opsrtoslem1  21969  opsrtoslem2  21970  lmfval  23126  lmbr  23152  lgsquadlem3  27300  perpln1  28644  outpasch  28689  ishpg  28693  axcontlem2  28899  wksfval  29544  wlkson  29591  pthsfval  29656  ispth  29658  dfadj2  31821  dmadjss  31823  cnvadj  31828  mpomptxf  32608  lsmsnorb2  33370  satfv0  35352  satfvsuclem1  35353  satfvsuclem2  35354  satfbrsuc  35360  satf0  35366  satf0suclem  35369  fmlasuc0  35378  fneer  36348  bj-dfmpoa  37113  bj-mpomptALT  37114  bj-brab2a1  37144  bj-imdiridlem  37180  bj-opabco  37183  opropabco  37725  cnvepres  38293  inxp2  38356  disjecxrn  38382  xrninxp  38385  xrninxp2  38386  rnxrnres  38392  rnxrncnvepres  38393  rnxrnidres  38394  dfcoss2  38411  dfcoss3  38412  cosscnv  38414  coss1cnvres  38415  coss2cnvepres  38416  1cossres  38427  dfcoels  38428  ressn2  38440  br1cosscnvxrn  38472  1cosscnvxrn  38473  coss0  38477  cossid  38478  dfssr2  38497  cmtfvalN  39210  cmtvalN  39211  cvrfval  39268  cvrval  39269  dicval2  41180  aks6d1c1p1rcl  42103  aks6d1c1rh  42120  fgraphopab  43199  fgraphxp  43200  modelaxreplem2  44976  mptssid  45242  dfnelbr2  47278  opabbrfex0d  47291  opabbrfexd  47293  upwlksfval  48127  xpsnopab  48149  mpomptx2  48327  upfval2  49170