MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elixp2 Structured version   Visualization version   GIF version

Theorem elixp2 8880
Description: Membership in an infinite Cartesian product. See df-ixp 8877 for discussion of the notation. (Contributed by NM, 28-Sep-2006.)
Assertion
Ref Expression
elixp2 (𝐹X𝑥𝐴 𝐵 ↔ (𝐹 ∈ V ∧ 𝐹 Fn 𝐴 ∧ ∀𝑥𝐴 (𝐹𝑥) ∈ 𝐵))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐹
Allowed substitution hint:   𝐵(𝑥)

Proof of Theorem elixp2
Dummy variable 𝑓 is distinct from all other variables.
StepHypRef Expression
1 fneq1 6630 . . . . 5 (𝑓 = 𝐹 → (𝑓 Fn 𝐴𝐹 Fn 𝐴))
2 fveq1 6878 . . . . . . 7 (𝑓 = 𝐹 → (𝑓𝑥) = (𝐹𝑥))
32eleq1d 2818 . . . . . 6 (𝑓 = 𝐹 → ((𝑓𝑥) ∈ 𝐵 ↔ (𝐹𝑥) ∈ 𝐵))
43ralbidv 3177 . . . . 5 (𝑓 = 𝐹 → (∀𝑥𝐴 (𝑓𝑥) ∈ 𝐵 ↔ ∀𝑥𝐴 (𝐹𝑥) ∈ 𝐵))
51, 4anbi12d 631 . . . 4 (𝑓 = 𝐹 → ((𝑓 Fn 𝐴 ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐵) ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥𝐴 (𝐹𝑥) ∈ 𝐵)))
6 dfixp 8878 . . . 4 X𝑥𝐴 𝐵 = {𝑓 ∣ (𝑓 Fn 𝐴 ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐵)}
75, 6elab2g 3667 . . 3 (𝐹 ∈ V → (𝐹X𝑥𝐴 𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥𝐴 (𝐹𝑥) ∈ 𝐵)))
87pm5.32i 575 . 2 ((𝐹 ∈ V ∧ 𝐹X𝑥𝐴 𝐵) ↔ (𝐹 ∈ V ∧ (𝐹 Fn 𝐴 ∧ ∀𝑥𝐴 (𝐹𝑥) ∈ 𝐵)))
9 elex 3492 . . 3 (𝐹X𝑥𝐴 𝐵𝐹 ∈ V)
109pm4.71ri 561 . 2 (𝐹X𝑥𝐴 𝐵 ↔ (𝐹 ∈ V ∧ 𝐹X𝑥𝐴 𝐵))
11 3anass 1095 . 2 ((𝐹 ∈ V ∧ 𝐹 Fn 𝐴 ∧ ∀𝑥𝐴 (𝐹𝑥) ∈ 𝐵) ↔ (𝐹 ∈ V ∧ (𝐹 Fn 𝐴 ∧ ∀𝑥𝐴 (𝐹𝑥) ∈ 𝐵)))
128, 10, 113bitr4i 302 1 (𝐹X𝑥𝐴 𝐵 ↔ (𝐹 ∈ V ∧ 𝐹 Fn 𝐴 ∧ ∀𝑥𝐴 (𝐹𝑥) ∈ 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 396  w3a 1087   = wceq 1541  wcel 2106  wral 3061  Vcvv 3474   Fn wfn 6528  cfv 6533  Xcixp 8876
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rab 3433  df-v 3476  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4320  df-if 4524  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-br 5143  df-opab 5205  df-rel 5677  df-cnv 5678  df-co 5679  df-dm 5680  df-iota 6485  df-fun 6535  df-fn 6536  df-fv 6541  df-ixp 8877
This theorem is referenced by:  fvixp  8881  ixpfn  8882  elixp  8883  ixpf  8899  resixp  8912  undifixp  8913  mptelixpg  8914  prdsbasprj  17402  xpsfrnel  17492  xpscf  17495  isssc  17751  isfuncd  17799  funcres2b  17831  dprdw  19841  ptrecube  36356  kelac1  41640  elixpconstg  43613  fvixp2  43733  rrxsnicc  44853  ioorrnopnxrlem  44859  hoiqssbllem1  45175  iinhoiicclem  45226  iunhoiioolem  45228  funcf2lem  47350
  Copyright terms: Public domain W3C validator