Theorem elrab 2962

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 2374	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2374	. 2 ⊢ Ⅎ𝑥𝐵
3		nfv 1576	. 2 ⊢ Ⅎ𝑥𝜓
4		elrab.1	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
5	1, 2, 3, 4	elrabf 2960	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1397   ∈ wcel 2202  {crab 2514

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rab 2519  df-v 2804

This theorem is referenced by:  elrab3  2963  elrabd  2964  elrab2  2965  ralrab  2967  rexrab  2969  rabsnt  3746  unimax  3927  ssintub  3946  intminss  3953  exmidexmid  4286  exmidsssnc  4293  rabxfrd  4566  ordtri2or2exmidlem  4624  onsucelsucexmidlem1  4626  sefvex  5660  ssimaex  5707  acexmidlem2  6015  elpmg  6833  ssfilem  7062  ssfilemd  7064  diffitest  7076  inffiexmid  7098  supubti  7198  suplubti  7199  ctssexmid  7349  sspw1or2  7403  exmidonfinlem  7404  finacn  7419  cc4f  7488  cc4n  7490  acnccim  7491  caucvgprlemladdfu  7897  caucvgprlemladdrl  7898  suplocexprlemmu  7938  suplocexprlemru  7939  suplocexprlemdisj  7940  suplocexprlemub  7943  nnindnn  8113  negf1o  8561  apsscn  8827  sup3exmid  9137  nnind  9159  peano2uz2  9587  peano5uzti  9588  dfuzi  9590  uzind  9591  uzind3  9593  eluz1  9759  uzind4  9822  supinfneg  9829  infsupneg  9830  eqreznegel  9848  elixx1  10132  elioo2  10156  elfz1  10248  zsupcl  10492  infssuzex  10494  infssuzcldc  10496  expcl2lemap  10814  expclzaplem  10826  expclzap  10827  expap0i  10834  expge0  10838  expge1  10839  hashennnuni  11042  wrdmap  11149  shftf  11395  reccn2ap  11878  dvdsdivcl  12416  divalgmod  12493  bitsval  12509  bitsfzolem  12520  bezoutlemsup  12585  dfgcd2  12590  uzwodc  12613  nnwosdc  12615  nninfctlemfo  12616  lcmgcdlem  12654  1nprm  12691  1idssfct  12692  isprm2  12694  phicl2  12791  hashdvds  12798  dvdsfi  12816  phisum  12818  odzval  12819  odzcllem  12820  odzdvds  12823  oddennn  13018  evenennn  13019  znnen  13024  ennnfonelemg  13029  ennnfonelemom  13034  ismhm  13549  issubm  13560  issubmd  13562  grplinv  13638  issubg  13765  isnsg  13794  isrim0  14181  issubrng  14219  issubrg  14241  islssm  14377  islssmg  14378  cnfldui  14609  mplelbascoe  14712  istopon  14743  epttop  14820  iscld  14833  isnei  14874  neipsm  14884  iscn  14927  iscnp  14929  txdis1cn  15008  ishmeo  15034  ispsmet  15053  ismet  15074  isxmet  15075  elblps  15120  elbl  15121  xmetxpbl  15238  reopnap  15276  divcnap  15295  elcncf  15303  cdivcncfap  15334  cnopnap  15341  divcncfap  15344  maxcncf  15345  mincncf  15346  ellimc3apf  15390  limccoap  15408  dvlemap  15410  dvidlemap  15421  dvidrelem  15422  dvidsslem  15423  dvcnp2cntop  15429  dvaddxxbr  15431  dvmulxxbr  15432  dvcoapbr  15437  dvcjbr  15438  dvrecap  15443  dveflem  15456  dvdsppwf1o  15719  lgsfle1  15744  lgsle1  15750  lgsdirprm  15769  lgsne0  15773  lgsquadlem1  15812  lgsquadlem2  15813  uhgrm  15935  upgrm  15957  upgr1or2  15958  umgredg2en  15966  umgrbien  15967  uhgredgm  15993  edgupgren  15998  edgumgren  15999  edgusgren  16020  usgruspgrben  16043  ushgredgedg  16083  ushgredgedgloop  16085  isclwwlk  16251  isclwwlkng  16263  clwwlknon  16286  eupth2lemsfi  16335  2omap  16620  pw1map  16622  subctctexmid  16627