Theorem elrab 2959

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1395   ∈ wcel 2200  {crab 2512

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rab 2517  df-v 2801

This theorem is referenced by:  elrab3  2960  elrabd  2961  elrab2  2962  ralrab  2964  rexrab  2966  rabsnt  3741  unimax  3921  ssintub  3940  intminss  3947  exmidexmid  4279  exmidsssnc  4286  rabxfrd  4559  ordtri2or2exmidlem  4617  onsucelsucexmidlem1  4619  sefvex  5647  ssimaex  5694  acexmidlem2  5997  elpmg  6809  ssfilem  7033  diffitest  7045  inffiexmid  7064  supubti  7162  suplubti  7163  ctssexmid  7313  exmidonfinlem  7367  finacn  7382  cc4f  7451  cc4n  7453  acnccim  7454  caucvgprlemladdfu  7860  caucvgprlemladdrl  7861  suplocexprlemmu  7901  suplocexprlemru  7902  suplocexprlemdisj  7903  suplocexprlemub  7906  nnindnn  8076  negf1o  8524  apsscn  8790  sup3exmid  9100  nnind  9122  peano2uz2  9550  peano5uzti  9551  dfuzi  9553  uzind  9554  uzind3  9556  eluz1  9722  uzind4  9779  supinfneg  9786  infsupneg  9787  eqreznegel  9805  elixx1  10089  elioo2  10113  elfz1  10205  zsupcl  10446  infssuzex  10448  infssuzcldc  10450  expcl2lemap  10768  expclzaplem  10780  expclzap  10781  expap0i  10788  expge0  10792  expge1  10793  hashennnuni  10996  wrdmap  11098  shftf  11336  reccn2ap  11819  dvdsdivcl  12356  divalgmod  12433  bitsval  12449  bitsfzolem  12460  bezoutlemsup  12525  dfgcd2  12530  uzwodc  12553  nnwosdc  12555  nninfctlemfo  12556  lcmgcdlem  12594  1nprm  12631  1idssfct  12632  isprm2  12634  phicl2  12731  hashdvds  12738  dvdsfi  12756  phisum  12758  odzval  12759  odzcllem  12760  odzdvds  12763  oddennn  12958  evenennn  12959  znnen  12964  ennnfonelemg  12969  ennnfonelemom  12974  ismhm  13489  issubm  13500  issubmd  13502  grplinv  13578  issubg  13705  isnsg  13734  isrim0  14119  issubrng  14157  issubrg  14179  islssm  14315  islssmg  14316  cnfldui  14547  mplelbascoe  14650  istopon  14681  epttop  14758  iscld  14771  isnei  14812  neipsm  14822  iscn  14865  iscnp  14867  txdis1cn  14946  ishmeo  14972  ispsmet  14991  ismet  15012  isxmet  15013  elblps  15058  elbl  15059  xmetxpbl  15176  reopnap  15214  divcnap  15233  elcncf  15241  cdivcncfap  15272  cnopnap  15279  divcncfap  15282  maxcncf  15283  mincncf  15284  ellimc3apf  15328  limccoap  15346  dvlemap  15348  dvidlemap  15359  dvidrelem  15360  dvidsslem  15361  dvcnp2cntop  15367  dvaddxxbr  15369  dvmulxxbr  15370  dvcoapbr  15375  dvcjbr  15376  dvrecap  15381  dveflem  15394  dvdsppwf1o  15657  lgsfle1  15682  lgsle1  15688  lgsdirprm  15707  lgsne0  15711  lgsquadlem1  15750  lgsquadlem2  15751  uhgrm  15872  upgrm  15894  upgr1or2  15895  umgredg2en  15903  umgrbien  15904  uhgredgm  15928  edgupgren  15933  edgumgren  15934  edgusgren  15955  usgruspgrben  15978  ushgredgedg  16018  ushgredgedgloop  16020  2omap  16318  pw1map  16320  subctctexmid  16325