Theorem opabbii 5152

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

Syntax hints:   ↔ wb 206   = wceq 1542  {copab 5147

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-opab 5148

This theorem is referenced by:  mptv  5191  2rbropap  5519  dfid4  5527  fconstmpt  5693  xpundi  5700  xpundir  5701  csbcnv  5838  cnvco  5840  resopab  5999  opabresid  6015  cnvi  6105  cnvun  6106  cnvxp  6121  cnvcnv3  6152  coundi  6211  coundir  6212  mptun  6644  fvopab6  6982  fmptsng  7123  fmptsnd  7124  cbvoprab1  7454  cbvoprab12  7456  dmoprabss  7471  mpomptx  7480  resoprab  7485  elrnmpores  7505  ov6g  7531  1st2val  7970  2nd2val  7971  dfoprab3s  8006  dfoprab3  8007  dfoprab4  8008  opabn1stprc  8011  mptmpoopabbrd  8033  fsplit  8067  mapsncnv  8841  xpcomco  9005  marypha2lem2  9349  oemapso  9603  ttrclresv  9638  leweon  9933  r0weon  9934  compsscnv  10293  fpwwe  10569  ltrelxr  11206  ltxrlt  11216  ltxr  13066  shftidt2  15043  prdsle  17425  prdsless  17426  prdsleval  17440  dfiso2  17739  joindm  18339  meetdm  18353  gaorb  19282  efgcpbllema  19729  frgpuplem  19747  dvdsrzring  21441  pjfval2  21689  ltbval  22021  ltbwe  22022  opsrle  22025  opsrtoslem1  22033  opsrtoslem2  22034  lmfval  23197  lmbr  23223  lgsquadlem3  27345  perpln1  28778  outpasch  28823  ishpg  28827  axcontlem2  29034  wksfval  29678  wlkson  29723  pthsfval  29787  ispth  29789  dfadj2  31956  dmadjss  31958  cnvadj  31963  mpomptxf  32751  lsmsnorb2  33452  satfv0  35540  satfvsuclem1  35541  satfvsuclem2  35542  satfbrsuc  35548  satf0  35554  satf0suclem  35557  fmlasuc0  35566  dfsuccf2  36123  fneer  36535  bj-dfmpoa  37430  bj-mpomptALT  37431  bj-brab2a1  37463  bj-imdiridlem  37499  bj-opabco  37502  opropabco  38045  xpv  38583  cnvepres  38625  inxp2  38696  disjecxrn  38733  xrninxp  38736  xrninxp2  38737  rnxrnres  38743  rnxrncnvepres  38744  rnxrnidres  38745  blockadjliftmap  38779  dfsucmap3  38784  dfsucmap4  38786  dfcoss2  38824  dfcoss3  38825  cosscnv  38827  coss1cnvres  38828  coss2cnvepres  38829  1cossres  38840  dfcoels  38841  ressn2  38853  br1cosscnvxrn  38885  1cosscnvxrn  38886  coss0  38890  cossid  38891  dfssr2  38900  dfpetparts2  39293  dfpeters2  39295  petseq  39297  cmtfvalN  39656  cmtvalN  39657  cvrfval  39714  cvrval  39715  dicval2  41625  aks6d1c1p1rcl  42547  aks6d1c1rh  42564  fgraphopab  43631  fgraphxp  43632  modelaxreplem2  45406  mptssid  45670  dfnelbr2  47721  opabbrfex0d  47734  opabbrfexd  47736  upwlksfval  48611  xpsnopab  48633  mpomptx2  48811  upfval2  49652