Theorem opabbii 5180

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570  {copab 5175

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-opab 5176

This theorem is used by:  mptv  5219  2rbropap  5551  dfid4  5559  fconstmpt  5725  xpundi  5732  xpundir  5733  cnvi  5873  csbcnv  5874  csbcnvOLD  5875  cnvco  5877  resopab  6038  opabresid  6054  cnvun  6141  cnvxp  6156  cnvcnv3  6188  coundi  6250  coundir  6251  mptun  6685  fvopab6  7028  fmptsng  7170  fmptsnd  7171  cbvoprab1  7503  cbvoprab12  7505  dmoprabss  7520  mpomptx  7529  resoprab  7534  elrnmpores  7554  ov6g  7580  1st2val  8016  2nd2val  8017  dfoprab3s  8052  dfoprab3  8053  dfoprab4  8054  opabn1stprc  8057  mptmpoopabbrd  8080  fsplit  8114  mapsncnv  8893  xpcomco  9058  marypha2lem2  9399  oemapso  9654  ttrclresv  9689  leweon  10007  r0weon  10008  compsscnv  10366  fpwwe  10642  ltrelxr  11281  ltxrlt  11291  ltxr  13151  shftidt2  15137  prdsle  17532  prdsless  17533  prdsleval  17547  dfiso2  17846  joindm  18446  meetdm  18460  gaorb  19400  efgcpbllema  19847  frgpuplem  19865  dvdsrzring  21640  pjfval2  21888  ltbval  22223  ltbwe  22224  opsrle  22227  opsrtoslem1  22235  opsrtoslem2  22236  lmfval  23418  lmbr  23444  lgsquadlem3  27575  perpln1  29019  outpasch  29066  ishpg  29070  tgaltai  29246  axcontlem2  29344  wksfval  29988  wlkson  30033  pthsfval  30097  ispth  30099  dfadj2  32266  dmadjss  32268  cnvadj  32273  mpomptxf  33052  lsmsnorb2  33728  satfv0  35863  satfvsuclem1  35864  satfvsuclem2  35865  satfbrsuc  35871  satf0  35877  satf0suclem  35880  fmlasuc0  35889  dfsuccf2  36446  fneer  36897  bj-dfmpoa  37793  bj-mpomptALT  37794  bj-brab2a1  37826  bj-imdiridlem  37862  bj-opabco  37865  opropabco  38408  xpv  38944  cnvepres  38986  inxp2  39057  disjecxrn  39094  xrninxp  39097  xrninxp2  39098  rnxrnres  39104  rnxrncnvepres  39105  rnxrnidres  39106  blockadjliftmap  39140  dfsucmap3  39145  dfsucmap4  39147  dfcoss2  39185  dfcoss3  39186  cosscnv  39188  coss1cnvres  39189  coss2cnvepres  39190  1cossres  39201  dfcoels  39202  ressn2  39214  br1cosscnvxrn  39246  1cosscnvxrn  39247  coss0  39251  cossid  39252  dfssr2  39261  dfpetparts2  39654  dfpeters2  39656  petseq  39658  cmtfvalN  40017  cmtvalN  40018  cvrfval  40075  cvrval  40076  dicval2  41986  aks6d1c1p1rcl  42908  aks6d1c1rh  42925  fgraphopab  43963  fgraphxp  43964  modelaxreplem2  45721  mptssid  45989  dfnelbr2  48043  opabbrfex0d  48056  opabbrfexd  48058  upwlksfval  48933  xpsnopab  48955  mpomptx2  49148  upfval2  49988