Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > elrabf | Structured version Visualization version GIF version |
Description: Membership in a restricted class abstraction, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable restrictions. (Contributed by NM, 21-Sep-2003.) |
Ref | Expression |
---|---|
elrabf.1 | ⊢ Ⅎ𝑥𝐴 |
elrabf.2 | ⊢ Ⅎ𝑥𝐵 |
elrabf.3 | ⊢ Ⅎ𝑥𝜓 |
elrabf.4 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
elrabf | ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex 3513 | . 2 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} → 𝐴 ∈ V) | |
2 | elex 3513 | . . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V) | |
3 | 2 | adantr 481 | . 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → 𝐴 ∈ V) |
4 | df-rab 3147 | . . . 4 ⊢ {𝑥 ∈ 𝐵 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)} | |
5 | 4 | eleq2i 2904 | . . 3 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ 𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)}) |
6 | elrabf.1 | . . . 4 ⊢ Ⅎ𝑥𝐴 | |
7 | elrabf.2 | . . . . . 6 ⊢ Ⅎ𝑥𝐵 | |
8 | 6, 7 | nfel 2992 | . . . . 5 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵 |
9 | elrabf.3 | . . . . 5 ⊢ Ⅎ𝑥𝜓 | |
10 | 8, 9 | nfan 1891 | . . . 4 ⊢ Ⅎ𝑥(𝐴 ∈ 𝐵 ∧ 𝜓) |
11 | eleq1 2900 | . . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) | |
12 | elrabf.4 | . . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
13 | 11, 12 | anbi12d 630 | . . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝜑) ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))) |
14 | 6, 10, 13 | elabgf 3663 | . . 3 ⊢ (𝐴 ∈ V → (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))) |
15 | 5, 14 | syl5bb 284 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))) |
16 | 1, 3, 15 | pm5.21nii 380 | 1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 = wceq 1528 Ⅎwnf 1775 ∈ wcel 2105 {cab 2799 Ⅎwnfc 2961 {crab 3142 Vcvv 3495 |
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: rabtru 3676 invdisjrabw 5043 invdisjrab 5044 rabxfrd 5309 f1ossf1o 6883 onminsb 7502 nnawordex 8253 tskwe 9368 rabssnn0fi 13344 iundisj 24078 iundisjf 30268 iundisjfi 30446 bnj1388 32203 sltval2 33061 phpreu 34758 poimirlem26 34800 rfcnpre3 41170 rfcnpre4 41171 uzwo4 41195 disjinfi 41334 allbutfiinf 41574 fsumiunss 41736 fnlimfvre 41835 stoweidlem26 42192 stoweidlem27 42193 stoweidlem31 42197 stoweidlem34 42200 stoweidlem51 42217 stoweidlem52 42218 stoweidlem59 42225 fourierdlem20 42293 fourierdlem79 42351 pimdecfgtioc 42874 smfpimcclem 42962 prmdvdsfmtnof1lem1 43593 |
Copyright terms: Public domain | W3C validator |