Theorem elrabi 2917

Description: Implication for the membership in a restricted class abstraction. (Contributed by Alexander van der Vekens, 31-Dec-2017.)

Assertion

Ref	Expression
elrabi	⊢ (𝐴 ∈ {𝑥 ∈ 𝑉 ∣ 𝜑} → 𝐴 ∈ 𝑉)

Distinct variable groups:   𝑥,𝐴   𝑥,𝑉

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem elrabi

Step	Hyp	Ref	Expression
1		clelab 2322	. . 3 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ ∃𝑥(𝑥 = 𝐴 ∧ (𝑥 ∈ 𝑉 ∧ 𝜑)))
2		eleq1 2259	. . . . . 6 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝑉 ↔ 𝐴 ∈ 𝑉))
3	2	anbi1d 465	. . . . 5 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝑉 ∧ 𝜑) ↔ (𝐴 ∈ 𝑉 ∧ 𝜑)))
4	3	simprbda 383	. . . 4 ⊢ ((𝑥 = 𝐴 ∧ (𝑥 ∈ 𝑉 ∧ 𝜑)) → 𝐴 ∈ 𝑉)
5	4	exlimiv 1612	. . 3 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ (𝑥 ∈ 𝑉 ∧ 𝜑)) → 𝐴 ∈ 𝑉)
6	1, 5	sylbi 121	. 2 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝐴 ∈ 𝑉)
7		df-rab 2484	. 2 ⊢ {𝑥 ∈ 𝑉 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}
8	6, 7	eleq2s 2291	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝑉 ∣ 𝜑} → 𝐴 ∈ 𝑉)

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1364  ∃wex 1506   ∈ wcel 2167  {cab 2182  {crab 2479

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-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-rab 2484

This theorem is referenced by:  ordtriexmidlem  4556  ordtri2or2exmidlem  4563  onsucelsucexmidlem  4566  ordsoexmid  4599  reg3exmidlemwe  4616  elfvmptrab1  5657  acexmidlemcase  5918  elovmporab  6125  elovmporab1w  6126  ssfirab  6999  exmidonfinlem  7263  cc4f  7339  genpelvl  7582  genpelvu  7583  suplocsrlempr  7877  nnindnn  7963  sup3exmid  8987  nnind  9009  supinfneg  9672  infsupneg  9673  supminfex  9674  ublbneg  9690  zsupcllemstep  10322  infssuzex  10326  infssuzledc  10327  hashinfuni  10872  bezoutlemsup  12187  uzwodc  12215  nninfctlemfo  12218  lcmgcdlem  12256  phisum  12420  oddennn  12620  evenennn  12621  znnen  12626  ennnfonelemg  12631  rrgval  13844  psrbagf  14250  txdis1cn  14540  reopnap  14808  divcnap  14827  limccl  14921  dvlemap  14942  dvaddxxbr  14963  dvmulxxbr  14964  dvcoapbr  14969  dvcjbr  14970  dvrecap  14975  dveflem  14988  sgmval  15245  0sgm  15247  sgmf  15248  sgmnncl  15250  dvdsppwf1o  15251  sgmppw  15254