Theorem elrab 2933

Description: Membership in a restricted class abstraction, using implicit substitution. (Contributed by NM, 21-May-1999.)

Hypothesis

Ref	Expression
elrab.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
elrab	⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))

Distinct variable groups:   𝜓,𝑥   𝑥,𝐴   𝑥,𝐵

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem elrab

Step	Hyp	Ref	Expression
1		nfcv 2349	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2349	. 2 ⊢ Ⅎ𝑥𝐵
3		nfv 1552	. 2 ⊢ Ⅎ𝑥𝜓
4		elrab.1	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
5	1, 2, 3, 4	elrabf 2931	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1373   ∈ wcel 2177  {crab 2489

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-rab 2494  df-v 2775

This theorem is referenced by:  elrab3  2934  elrabd  2935  elrab2  2936  ralrab  2938  rexrab  2940  rabsnt  3713  unimax  3890  ssintub  3909  intminss  3916  exmidexmid  4248  exmidsssnc  4255  rabxfrd  4524  ordtri2or2exmidlem  4582  onsucelsucexmidlem1  4584  sefvex  5610  ssimaex  5653  acexmidlem2  5954  elpmg  6764  ssfilem  6987  diffitest  6999  inffiexmid  7018  supubti  7116  suplubti  7117  ctssexmid  7267  exmidonfinlem  7317  finacn  7332  cc4f  7401  cc4n  7403  acnccim  7404  caucvgprlemladdfu  7810  caucvgprlemladdrl  7811  suplocexprlemmu  7851  suplocexprlemru  7852  suplocexprlemdisj  7853  suplocexprlemub  7856  nnindnn  8026  negf1o  8474  apsscn  8740  sup3exmid  9050  nnind  9072  peano2uz2  9500  peano5uzti  9501  dfuzi  9503  uzind  9504  uzind3  9506  eluz1  9672  uzind4  9729  supinfneg  9736  infsupneg  9737  eqreznegel  9755  elixx1  10039  elioo2  10063  elfz1  10155  zsupcl  10396  infssuzex  10398  infssuzcldc  10400  expcl2lemap  10718  expclzaplem  10730  expclzap  10731  expap0i  10738  expge0  10742  expge1  10743  hashennnuni  10946  wrdmap  11047  shftf  11216  reccn2ap  11699  dvdsdivcl  12236  divalgmod  12313  bitsval  12329  bitsfzolem  12340  bezoutlemsup  12405  dfgcd2  12410  uzwodc  12433  nnwosdc  12435  nninfctlemfo  12436  lcmgcdlem  12474  1nprm  12511  1idssfct  12512  isprm2  12514  phicl2  12611  hashdvds  12618  dvdsfi  12636  phisum  12638  odzval  12639  odzcllem  12640  odzdvds  12643  oddennn  12838  evenennn  12839  znnen  12844  ennnfonelemg  12849  ennnfonelemom  12854  ismhm  13368  issubm  13379  issubmd  13381  grplinv  13457  issubg  13584  isnsg  13613  isrim0  13998  issubrng  14036  issubrg  14058  islssm  14194  islssmg  14195  cnfldui  14426  mplelbascoe  14529  istopon  14560  epttop  14637  iscld  14650  isnei  14691  neipsm  14701  iscn  14744  iscnp  14746  txdis1cn  14825  ishmeo  14851  ispsmet  14870  ismet  14891  isxmet  14892  elblps  14937  elbl  14938  xmetxpbl  15055  reopnap  15093  divcnap  15112  elcncf  15120  cdivcncfap  15151  cnopnap  15158  divcncfap  15161  maxcncf  15162  mincncf  15163  ellimc3apf  15207  limccoap  15225  dvlemap  15227  dvidlemap  15238  dvidrelem  15239  dvidsslem  15240  dvcnp2cntop  15246  dvaddxxbr  15248  dvmulxxbr  15249  dvcoapbr  15254  dvcjbr  15255  dvrecap  15260  dveflem  15273  dvdsppwf1o  15536  lgsfle1  15561  lgsle1  15567  lgsdirprm  15586  lgsne0  15590  lgsquadlem1  15629  lgsquadlem2  15630  uhgrm  15749  upgrm  15771  upgr1or2  15772  umgredg2en  15780  umgrbien  15781  2omap  16071  pw1map  16073  subctctexmid  16078