Theorem opabbii 5174

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

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-opab 5170

This theorem is referenced by:  mptv  5213  2rbropap  5526  dfid4  5534  fconstmpt  5700  xpundi  5707  xpundir  5708  inxpOLD  5796  csbcnv  5847  cnvco  5849  resopab  6005  opabresid  6021  cnvi  6114  cnvun  6115  cnvxp  6130  cnvcnv3  6161  coundi  6220  coundir  6221  mptun  6664  fvopab6  7002  fmptsng  7142  fmptsnd  7143  cbvoprab1  7476  cbvoprab12  7478  dmoprabss  7493  mpomptx  7502  resoprab  7507  elrnmpores  7527  ov6g  7553  1st2val  7996  2nd2val  7997  dfoprab3s  8032  dfoprab3  8033  dfoprab4  8034  opabn1stprc  8037  mptmpoopabbrd  8059  mptmpoopabbrdOLD  8060  mptmpoopabbrdOLDOLD  8062  fsplit  8096  mapsncnv  8866  xpcomco  9031  marypha2lem2  9387  oemapso  9635  ttrclresv  9670  leweon  9964  r0weon  9965  compsscnv  10324  fpwwe  10599  ltrelxr  11235  ltxrlt  11244  ltxr  13075  shftidt2  15047  prdsle  17425  prdsless  17426  prdsleval  17440  dfiso2  17734  joindm  18334  meetdm  18348  gaorb  19239  efgcpbllema  19684  frgpuplem  19702  dvdsrzring  21371  pjfval2  21618  ltbval  21950  ltbwe  21951  opsrle  21954  opsrtoslem1  21962  opsrtoslem2  21963  lmfval  23119  lmbr  23145  lgsquadlem3  27293  perpln1  28637  outpasch  28682  ishpg  28686  axcontlem2  28892  wksfval  29537  wlkson  29584  pthsfval  29649  ispth  29651  dfadj2  31814  dmadjss  31816  cnvadj  31821  mpomptxf  32601  lsmsnorb2  33363  satfv0  35345  satfvsuclem1  35346  satfvsuclem2  35347  satfbrsuc  35353  satf0  35359  satf0suclem  35362  fmlasuc0  35371  fneer  36341  bj-dfmpoa  37106  bj-mpomptALT  37107  bj-brab2a1  37137  bj-imdiridlem  37173  bj-opabco  37176  opropabco  37718  cnvepres  38286  inxp2  38349  disjecxrn  38375  xrninxp  38378  xrninxp2  38379  rnxrnres  38385  rnxrncnvepres  38386  rnxrnidres  38387  dfcoss2  38404  dfcoss3  38405  cosscnv  38407  coss1cnvres  38408  coss2cnvepres  38409  1cossres  38420  dfcoels  38421  ressn2  38433  br1cosscnvxrn  38465  1cosscnvxrn  38466  coss0  38470  cossid  38471  dfssr2  38490  cmtfvalN  39203  cmtvalN  39204  cvrfval  39261  cvrval  39262  dicval2  41173  aks6d1c1p1rcl  42096  aks6d1c1rh  42113  fgraphopab  43192  fgraphxp  43193  modelaxreplem2  44969  mptssid  45235  dfnelbr2  47274  opabbrfex0d  47287  opabbrfexd  47289  upwlksfval  48123  xpsnopab  48145  mpomptx2  48323  upfval2  49166