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 3363 | . 2 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)) |
3 | 2 | baib 944 | 1 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 = wceq 1483 ∈ wcel 1990 {crab 2916 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-rab 2921 df-v 3202 |
This theorem is referenced by: unimax 4473 fnelfp 6441 fnelnfp 6443 fnse 7294 fin23lem30 9164 isf32lem5 9179 negn0 10459 ublbneg 11773 supminf 11775 sadval 15178 smuval 15203 dvdslcm 15311 dvdslcmf 15344 isprm2lem 15394 isacs1i 16318 isinito 16650 istermo 16651 subgacs 17629 nsgacs 17630 odngen 17992 lssacs 18967 mretopd 20896 txkgen 21455 xkoco1cn 21460 xkoco2cn 21461 xkoinjcn 21490 ordthmeolem 21604 shft2rab 23276 sca2rab 23280 lhop1lem 23776 ftalem5 24803 vmasum 24941 israg 25592 ebtwntg 25862 eupth2lem3lem3 27090 eupth2lem3lem4 27091 eupth2lem3lem6 27093 tgoldbachgt 30741 cvmliftmolem1 31263 neibastop3 32357 fdc 33541 pclvalN 35176 dvhb1dimN 36274 hdmaplkr 37205 diophren 37377 islmodfg 37639 sdrgacs 37771 fsovcnvlem 38307 ntrneiel 38379 radcnvrat 38513 supminfxr 39694 stoweidlem34 40251 |
Copyright terms: Public domain | W3C validator |