Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > elrab3 | Structured version Visualization version GIF version |
Description: Membership in a restricted class abstraction, using implicit substitution. (Contributed by NM, 5-Oct-2006.) |
Ref | Expression |
---|---|
elrab.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
elrab3 | ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elrab.1 | . . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
2 | 1 | elrab 3679 | . 2 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)) |
3 | 2 | baib 536 | 1 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 = wceq 1528 ∈ wcel 2105 {crab 3142 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-rab 3147 df-v 3497 |
This theorem is referenced by: unimax 4867 fnelfp 6930 fnelnfp 6932 fnse 7818 fin23lem30 9753 isf32lem5 9768 negn0 11058 ublbneg 12322 supminf 12324 sadval 15795 smuval 15820 dvdslcm 15932 dvdslcmf 15965 isprm2lem 16015 isacs1i 16918 isinito 17250 istermo 17251 subgacs 18253 nsgacs 18254 odngen 18633 sdrgacs 19511 lssacs 19670 mretopd 21630 txkgen 22190 xkoco1cn 22195 xkoco2cn 22196 xkoinjcn 22225 ordthmeolem 22339 shft2rab 24038 sca2rab 24042 lhop1lem 24539 ftalem5 25582 vmasum 25720 israg 26411 ebtwntg 26696 eupth2lem3lem3 27937 eupth2lem3lem4 27938 eupth2lem3lem6 27940 cycpmco2lem1 30696 cycpmco2lem4 30699 cycpmco2 30703 tgoldbachgt 31834 cvmliftmolem1 32426 neibastop3 33608 fdc 34903 pclvalN 36908 dvhb1dimN 38004 hdmaplkr 38931 diophren 39290 islmodfg 39549 fsovcnvlem 40239 ntrneiel 40311 radcnvrat 40526 supminfxr 41620 stoweidlem34 42200 |
Copyright terms: Public domain | W3C validator |